fix bug #2447 in congruence

6 files changed, 19 insertions, 14 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 858c80f296..b74b1faca0 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -504,8 +504,8 @@ let f_equal =
 	  end
       | _ -> Proofview.tclUNIT ()
       end
-      begin function
+      begin function (e, info) -> match e with
         | Type_errors.TypeError _ -> Proofview.tclUNIT ()
-        | e -> Proofview.tclZERO e
+        | e -> Proofview.tclZERO ~info e
       end
   end
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 43fefc4c6c..c8214ada8e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -74,9 +74,10 @@ let do_observe_tac s tac g =
     ignore(Stack.pop debug_queue);
     v
   with reraise ->
+    let reraise = Errors.push reraise in
     if not (Stack.is_empty debug_queue)
-    then print_debug_queue true (Cerrors.process_vernac_interp_error reraise);
-    raise reraise
+    then print_debug_queue true (fst (Cerrors.process_vernac_interp_error reraise));
+    iraise reraise
 
 let observe_tac_stream s tac g =
   if do_observe ()
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 71da59c499..1051cae75f 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -186,7 +186,7 @@ END
 
 
 let warning_error names e =
-  let e = Cerrors.process_vernac_interp_error e in
+  let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in
   match e with
     | Building_graph e ->
 	Pp.msg_warning
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2ce9f4f616..6dbd61cfdd 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -217,6 +217,8 @@ let prepare_body ((name,_,args,types,_),_) rt =
   let fun_args,rt' = chop_rlambda_n n rt in
   (fun_args,rt')
 
+let process_vernac_interp_error e =
+  fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))
 
 let derive_inversion fix_names =
   try
@@ -243,23 +245,23 @@ let derive_inversion fix_names =
 	   fix_names
 	)
     with e when Errors.noncritical e ->
-      let e' = Cerrors.process_vernac_interp_error e in
+      let e' = process_vernac_interp_error e in
       msg_warning
 	(str "Cannot build inversion information" ++
 	   if do_observe () then (fnl() ++ Errors.print e') else mt ())
   with e when Errors.noncritical e -> ()
 
 let warning_error names e =
-  let e = Cerrors.process_vernac_interp_error e in
+  let e = process_vernac_interp_error e in
   let e_explain e =
     match e with
       | ToShow e -> 
-	let e = Cerrors.process_vernac_interp_error e in
+	let e = process_vernac_interp_error e in
 	spc () ++ Errors.print e
       | _ -> 
 	if do_observe () 
 	then 
-	  let e = Cerrors.process_vernac_interp_error e in 
+	  let e = process_vernac_interp_error e in 
 	  (spc () ++ Errors.print e) 
 	else mt ()
   in
@@ -277,7 +279,7 @@ let warning_error names e =
     | _ -> raise e
 
 let error_error names e =
-  let e = Cerrors.process_vernac_interp_error e in
+  let e = process_vernac_interp_error e in
   let e_explain e =
     match e with
       | ToShow e -> spc () ++ Errors.print e
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index e07bce69c9..8a6c8430fd 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -68,10 +68,11 @@ let do_observe_tac s tac g =
     let v = tac g in
     msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
   with reraise ->
+    let reraise = Errors.push reraise in
     let e = Cerrors.process_vernac_interp_error reraise in
     msgnl (str "observation "++ s++str " raised exception " ++
-	     Errors.print e ++ str " on goal " ++ goal );
-    raise reraise;;
+	     Errors.iprint e ++ str " on goal " ++ goal );
+    iraise reraise;;
 
 
 let observe_tac_strm s tac g =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index a38764c5bd..a466e1089e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -236,9 +236,10 @@ let do_observe_tac s tac g =
     ignore(Stack.pop debug_queue);
     v
   with reraise ->
+    let reraise = Errors.push reraise in
     if not (Stack.is_empty debug_queue)
-    then print_debug_queue true (Cerrors.process_vernac_interp_error reraise);
-    raise reraise
+    then print_debug_queue true (fst (Cerrors.process_vernac_interp_error reraise));
+    iraise reraise
 
 let observe_tac s tac g =
   if do_observe ()