diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index cbf27b0320..9070e26179 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -340,12 +340,13 @@ val generalize_gen : ((occurrences * constr) * name) list -> tactic val generalize_dep : constr -> tactic val conv : constr -> constr -> tactic +val resolve_classes : tactic val tclABSTRACT : identifier option -> tactic -> tactic val admit_as_an_axiom : tactic -val abstract_generalize : identifier -> tactic +val abstract_generalize : identifier -> ?generalize_vars:bool -> tactic val register_general_multi_rewrite : (bool -> evars_flag -> constr with_ebindings -> clause -> tactic) -> unit |