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/cc/cctac.mli | |
| parent | bec752e2c354ad0cf939f875586a4db2189bd471 (diff) | |
Congruence: don't replace error messages by "congruence failed"
Fix #13595
Diffstat (limited to 'plugins/cc/cctac.mli')
| -rw-r--r-- | plugins/cc/cctac.mli | 2 |
1 files changed, 0 insertions, 2 deletions
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 |