From 02f8a5fc7d445ee093bc80663646cfea0a915e6d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Apr 2017 17:36:35 +0200
Subject: Removing tactic compatibility layer in congruence.

---
 plugins/cc/cctac.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/cc/cctac.mli')

diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index de6eb982ee..5099d847b0 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -14,7 +14,7 @@ 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
 
-- 
cgit v1.2.3