diff options
| author | corbinea | 2009-10-27 09:05:29 +0000 |
|---|---|---|
| committer | corbinea | 2009-10-27 09:05:29 +0000 |
| commit | 7a9a59d693c9f3a60db10325ae72ff1675948695 (patch) | |
| tree | 6dc09033899609a742aebfd744d66e416d8d5766 | |
| parent | 722d0c21cb2f8da64b1c54f854c8dc401edd25e6 (diff) | |
fix previous commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12424 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/decl_proof_instr.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli index ada5e74489..1cfcfedf14 100644 --- a/tactics/decl_proof_instr.mli +++ b/tactics/decl_proof_instr.mli @@ -65,13 +65,8 @@ val build_dep_clause : Term.types Decl_expr.statement list -> (Term.types Decl_expr.statement, Term.types Decl_expr.or_thesis) Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types -<<<<<<< HEAD:tactics/decl_proof_instr.mli -val register_dep_subcase : - Names.identifier * int -> -======= val register_dep_subcase : Names.identifier * (int * int) -> ->>>>>>> ada3fb4... fixed czar bug with parametric inductives:tactics/decl_proof_instr.mli Environ.env -> Decl_mode.per_info -> Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind |