From 915c8f15965fe8e7ee9d02a663fd890ef80539ad Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 23 Apr 2015 14:22:42 +0200
Subject: Using tclZEROMSG instead of tclZERO in several places.

---
 plugins/cc/cctac.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/cc')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 8884aef1c..05f4c4903 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -302,9 +302,9 @@ let rec proof_tac p : unit Proofview.tactic =
   	     Tacticals.New.tclFIRST
 	       [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2);
 		reflexivity;
-                Proofview.tclZERO (UserError ("Congruence" ,
+                Tacticals.New.tclZEROMSG
 		    (Pp.str
-		       "I don't know how to handle dependent equality")))]]
+		       "I don't know how to handle dependent equality")]]
   | Inject (prf,cstr,nargs,argind) ->
 	 let ti=constr_of_term prf.p_lhs in
 	 let tj=constr_of_term prf.p_rhs in
-- 
cgit v1.2.3