diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 5b03a79dd..f3da4a8c9 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -46,7 +46,7 @@ exception Bound val introduction : identifier -> tactic val refine : constr -> tactic -val convert_concl : constr -> tactic +val convert_concl : constr -> cast_kind -> tactic val convert_hyp : named_declaration -> tactic val thin : identifier list -> tactic val mutual_fix : @@ -110,8 +110,8 @@ val exact_proof : Topconstr.constr_expr -> tactic type tactic_reduction = env -> evar_map -> constr -> constr val reduct_in_hyp : tactic_reduction -> hyp_location -> tactic -val reduct_option : tactic_reduction -> simple_clause -> tactic -val reduct_in_concl : tactic_reduction -> tactic +val reduct_option : tactic_reduction * cast_kind -> simple_clause -> tactic +val reduct_in_concl : tactic_reduction * cast_kind -> tactic val change_in_concl : constr occurrences option -> constr -> tactic val change_in_hyp : constr occurrences option -> constr -> hyp_location -> tactic @@ -124,9 +124,10 @@ val hnf_option : simple_clause -> tactic val simpl_in_concl : tactic val simpl_in_hyp : hyp_location -> tactic val simpl_option : simple_clause -> tactic -val normalise_in_concl: tactic +val normalise_in_concl : tactic val normalise_in_hyp : hyp_location -> tactic val normalise_option : simple_clause -> tactic +val normalise_vm_in_concl : tactic val unfold_in_concl : (int list * evaluable_global_reference) list -> tactic val unfold_in_hyp : (int list * evaluable_global_reference) list -> hyp_location -> tactic @@ -250,3 +251,4 @@ val generalize_dep : constr -> tactic val tclABSTRACT : identifier option -> tactic -> tactic val admit_as_an_axiom : tactic + |