diff options
| -rw-r--r-- | ltac/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 13 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
3 files changed, 8 insertions, 9 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index e03cc675e7..451e0987b0 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -582,7 +582,7 @@ END during dependent induction. For internal use. *) TACTIC EXTEND specialize_eqs -[ "specialize_eqs" hyp(id) ] -> [ Proofview.V82.tactic (specialize_eqs id) ] +[ "specialize_eqs" hyp(id) ] -> [ specialize_eqs id ] END (**********************************************************************) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 547c361642..59e6a1c82a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3698,13 +3698,12 @@ let specialize_eqs id gl = else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl -let specialize_eqs id gl = - if - (try ignore(Proofview.V82.of_tactic (clear [id]) gl); false - with e when Errors.noncritical e -> true) - then - tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl - else specialize_eqs id gl +let specialize_eqs id = Proofview.Goal.nf_enter { enter = begin fun gl -> + let msg = str "Specialization not allowed on dependent hypotheses" in + Proofview.tclOR (clear [id]) + (fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () -> + Proofview.V82.tactic (specialize_eqs id) +end } let occur_rel n c = let res = not (noccurn n c) in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index eb041e2a0b..6987e5b70e 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 |