diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 22:24:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 22:26:05 +0200 |
| commit | fd5898afa9a89ca61f87cdeca4ae982a024e4d4b (patch) | |
| tree | eb01be157606bbad65c1f68b9dbfd3ac51c38ef8 /tactics/tactics.mli | |
| parent | c6a16e8cc607f70f519f3ebbd5856b8ff501d782 (diff) | |
Put the "specialize_eq" tactic in the monad.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index eb041e2a0..6987e5b70 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -397,7 +397,7 @@ val unify : ?state:Names.transparent_state -> constr -> constr -> unit val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic -val specialize_eqs : Id.t -> tactic +val specialize_eqs : Id.t -> unit Proofview.tactic val general_rewrite_clause : (bool -> evars_flag -> constr with_bindings -> clause -> unit Proofview.tactic) Hook.t |