diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/cc/cctac.ml | 16 | ||||
| -rw-r--r-- | plugins/cc/cctac.mli | 2 |
2 files changed, 8 insertions, 10 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 12f80a17ed..499c9684b2 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -450,10 +450,14 @@ let cc_tactic depth additionnal_terms = str " Try " ++ hov 8 begin - str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(") - pr_missing terms_to_complete ++ str ")\"," + str "\"congruence with (" ++ + prlist_with_sep + (fun () -> str ")" ++ spc () ++ str "(") + pr_missing terms_to_complete ++ + str ")\"," end ++ - str " replacing metavariables by arbitrary terms.") in + fnl() ++ str " replacing metavariables by arbitrary terms") + in Tacticals.New.tclFAIL 0 msg | Contradiction dis -> let env = Proofview.Goal.env gl in @@ -471,13 +475,9 @@ let cc_tactic depth additionnal_terms = convert_to_hyp_tac ida ta idb tb p end -let cc_fail = - Tacticals.New.tclZEROMSG (Pp.str "congruence failed.") let congruence_tac depth l = - Tacticals.New.tclORELSE - (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l)) - cc_fail + Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l) (* Beware: reflexivity = constructor 1 = apply refl_equal might be slow now, let's rather do something equivalent diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index 52fc3acb6f..79c7d2c676 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -14,8 +14,6 @@ val proof_tac: Ccproof.proof -> unit Proofview.tactic val cc_tactic : int -> constr list -> unit Proofview.tactic -val cc_fail : unit Proofview.tactic - val congruence_tac : int -> constr list -> unit Proofview.tactic val f_equal : unit Proofview.tactic |