diff options
Diffstat (limited to 'tactics/decl_proof_instr.mli')
| -rw-r--r-- | tactics/decl_proof_instr.mli | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli index a05c36e93..ada5e7448 100644 --- a/tactics/decl_proof_instr.mli +++ b/tactics/decl_proof_instr.mli @@ -42,21 +42,21 @@ val execute_cases : (Names.Idset.elt * (Term.constr option * Term.constr list) list) list -> Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic -val tree_of_pats : - identifier * int -> (Rawterm.cases_pattern*recpath) list list -> +val tree_of_pats : + identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list -> split_tree -val add_branch : - identifier * int -> (Rawterm.cases_pattern*recpath) list list -> +val add_branch : + identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list -> split_tree -> split_tree val append_branch : - identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list -> + identifier *(int * int) -> int -> (Rawterm.cases_pattern*recpath) list list -> (Names.Idset.t * Decl_mode.split_tree) option -> (Names.Idset.t * Decl_mode.split_tree) option val append_tree : - identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list -> + identifier * (int * int) -> int -> (Rawterm.cases_pattern*recpath) list list -> split_tree -> split_tree val build_dep_clause : Term.types Decl_expr.statement list -> @@ -65,8 +65,13 @@ 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 @@ -116,3 +121,4 @@ val init_tree: (Names.Idset.t * Decl_mode.split_tree) option) -> Decl_mode.split_tree +val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit |