diff options
Diffstat (limited to 'plugins/cc/cctac.mli')
| -rw-r--r-- | plugins/cc/cctac.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index de6eb982e..b4bb62be8 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -8,13 +8,12 @@ (************************************************************************) open EConstr -open Proof_type val proof_tac: Ccproof.proof -> unit Proofview.tactic val cc_tactic : int -> constr list -> unit Proofview.tactic -val cc_fail : tactic +val cc_fail : unit Proofview.tactic val congruence_tac : int -> constr list -> unit Proofview.tactic |