diff options
| author | Gaëtan Gilbert | 2020-12-08 10:33:42 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-12-08 10:33:42 +0100 |
| commit | f4af5d4b09f262ef6388a2c0eeed85bf9b7ab3f9 (patch) | |
| tree | b2ec6bdef7f4642b2ff04ecd4176938a05a4cbbf /plugins | |
| parent | bec752e2c354ad0cf939f875586a4db2189bd471 (diff) | |
Congruence: don't replace error messages by "congruence failed"
Fix #13595
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 |