Fixing bugs #2347 (part 2) and #2388: error message printing was done

too late, in a global environment which was no longer the correct one,
leading to the failure of error printing (hence an anomaly) in case
the command modified the state in several steps.

Now, errors raised by vernac commands are processed in the same
(intermediate) state they were raised from, just before rolling back
to the original state.

that modify the state in several
Now, errors raised by vernac commands that modify the state in several
steps (say S1, S2, ..., Sn) are processed in the state they were
produced in (S1, S2, ... Sn-1),

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13431 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 74 insertions, 50 deletions

diff --git a/library/states.ml b/library/states.ml
index b7c66abf5..4619b3b53 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -28,12 +28,12 @@ let (extern_state,intern_state) =
 
 (* Rollback. *)
 
-let with_heavy_rollback f x =
+let with_heavy_rollback f h x =
   let st = freeze () in
   try
     f x
   with reraise ->
-    (unfreeze st; raise reraise)
+    let e = h reraise in (unfreeze st; raise e)
 
 let with_state_protection f x =
   let st = freeze () in
diff --git a/library/states.mli b/library/states.mli
index 70d139d36..4f114d576 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -25,7 +25,7 @@ val unfreeze : state -> unit
 (** [with_heavy_rollback f x] applies [f] to [x] and restores the
   state of the whole system as it was before the evaluation if an exception
   is raised. *)
-val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
+val with_heavy_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b
 
 (** [with_state_protection f x] applies [f] to [x] and restores the
   state of the whole system as it was before the evaluation of f *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/shouldsucceed/2388.v
new file mode 100644
index 000000000..c79267119
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2388.v
@@ -0,0 +1,10 @@
+(* Error message was not printed in the correct environment *)
+
+Fail Parameters (A:Prop) (a:A A).
+
+(* This is a variant (reported as part of bug #2347) *)
+
+Require Import EquivDec.                                              
+Fail Program Instance bool_eq_eqdec : EqDec bool eq := 
+   {equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}.
+
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 0d2111f8a..a34afda50 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -26,6 +26,8 @@ let guill s = "\""^s^"\""
 let where s =
   if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
 
+exception EvaluatedError of std_ppcmds * exn option
+
 (* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *)
 
 let rec explain_exn_default_aux anomaly_string report_fn = function
@@ -63,6 +65,26 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
       hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ())
   | Sys.Break ->
       hov 0 (fnl () ++ str "User interrupt.")
+  | Assert_failure (s,b,e) ->
+      hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
+	       (if s = "" then mt ()
+		else
+		  (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
+		   str ", characters " ++ int e ++ str "-" ++
+		   int (e+6) ++ str ")")) ++
+	       report_fn ())
+  | EvaluatedError (msg,None) ->
+      msg
+  | EvaluatedError (msg,Some reraise) ->
+      msg ++ explain_exn_default_aux anomaly_string report_fn reraise
+  | reraise ->
+      hov 0 (anomaly_string () ++ str "Uncaught exception " ++
+	       str (Printexc.to_string reraise) ++ report_fn ())
+
+let wrap_vernac_error strm =
+  EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None)
+
+let rec process_vernac_interp_error = function
   | Univ.UniverseInconsistency (o,u,v) ->
       let msg =
 	if !Constrextern.print_universes then
@@ -71,59 +93,48 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
 	  ++ spc() ++ Univ.pr_uni v ++ str")"
 	else
 	  mt() in
-      hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".")
+      wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".")
   | TypeError(ctx,te) ->
-      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te)
+      wrap_vernac_error (Himsg.explain_type_error ctx te)
   | PretypeError(ctx,te) ->
-      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te)
+      wrap_vernac_error (Himsg.explain_pretype_error ctx te)
   | Typeclasses_errors.TypeClassError(env, te) ->
-      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_typeclass_error env te)
+      wrap_vernac_error (Himsg.explain_typeclass_error env te)
   | InductiveError e ->
-      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e)
+      wrap_vernac_error (Himsg.explain_inductive_error e)
   | RecursionSchemeError e ->
-      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e)
-  | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () ->
-      explain_exn_default_aux anomaly_string report_fn exc
-  | Proof_type.LtacLocated (s,exc) ->
-      hov 0 (Himsg.explain_ltac_call_trace s ++ fnl ()
-             ++ explain_exn_default_aux anomaly_string report_fn exc)
+      wrap_vernac_error (Himsg.explain_recursion_scheme_error e)
   | Cases.PatternMatchingError (env,e) ->
-      hov 0
-	(str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e)
+      wrap_vernac_error (Himsg.explain_pattern_matching_error env e)
   | Tacred.ReductionTacticError e ->
-      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_reduction_tactic_error e)
+      wrap_vernac_error (Himsg.explain_reduction_tactic_error e)
   | Logic.RefinerError e ->
-      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e)
+      wrap_vernac_error (Himsg.explain_refiner_error e)
   | Nametab.GlobalizationError q ->
-      hov 0 (str "Error:" ++ spc () ++
-	       str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
-	       spc () ++ str "was not found" ++
-	       spc () ++ str "in the current" ++ spc () ++ str "environment.")
+      wrap_vernac_error
+        (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
+	 spc () ++ str "was not found" ++
+	 spc () ++ str "in the current" ++ spc () ++ str "environment.")
   | Nametab.GlobalizationConstantError q ->
-      hov 0 (str "Error:" ++ spc () ++
-	       str "No constant of this name:" ++ spc () ++
-               Libnames.pr_qualid q ++ str ".")
+      wrap_vernac_error
+        (str "No constant of this name:" ++ spc () ++
+         Libnames.pr_qualid q ++ str ".")
   | Refiner.FailError (i,s) ->
-      hov 0 (str "Error: Tactic failure" ++
+      EvaluatedError (hov 0 (str "Error: Tactic failure" ++
                 (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++
-                if i=0 then str "." else str " (level " ++ int i ++ str").")
-  | Loc.Exc_located (loc,exc) ->
-      hov 0 ((if loc = dummy_loc then (mt ())
-               else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
-               ++ explain_exn_default_aux anomaly_string report_fn exc)
-  | Assert_failure (s,b,e) ->
-      hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
-	       (if s = "" then mt ()
-		else
-		  (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
-		   str ", characters " ++ int e ++ str "-" ++
-		   int (e+6) ++ str ")")) ++
-	       report_fn ())
+                if i=0 then str "." else str " (level " ++ int i ++ str")."),
+                None)
   | AlreadyDeclared msg ->
-      hov 0 (str "Error: " ++ msg ++ str ".")
-  | reraise ->
-      hov 0 (anomaly_string () ++ str "Uncaught exception " ++
-	       str (Printexc.to_string reraise) ++ report_fn ())
+      wrap_vernac_error (msg ++ str ".")
+  | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () ->
+      process_vernac_interp_error exc
+  | Proof_type.LtacLocated (s,exc) ->
+      EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()),
+        Some (process_vernac_interp_error exc))
+  | Loc.Exc_located (loc,exc) ->
+      Loc.Exc_located (loc,process_vernac_interp_error exc)
+  | exc ->
+      exc
 
 let anomaly_string () = str "Anomaly: "
 
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 8dc7e7a79..0dae61f4a 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -15,10 +15,14 @@ val print_loc : loc -> std_ppcmds
 
 val explain_exn : exn -> std_ppcmds
 
-(** Same, but will re-raise all anomalies instead of explaining them *)
+(** Precompute errors raised during vernac interpretation *)
 
 val explain_exn_no_anomaly : exn -> std_ppcmds
 
+(** Pre-explain a vernac interpretation error *)
+
+val process_vernac_interp_error : exn -> exn
+
 (** For debugging purpose (?), the explain function can be twicked *)
 
 val explain_exn_function : (exn -> std_ppcmds) ref
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f84097a16..aef772676 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -197,7 +197,10 @@ let rec vernac_com interpfun (loc,com) =
 	  with e -> stop(); raise e
 	end
 
-    | v -> if not !just_parsing then interpfun v
+    | v ->
+        if not !just_parsing then
+          States.with_heavy_rollback interpfun
+            Cerrors.process_vernac_interp_error v
 
   in
     try
@@ -236,13 +239,10 @@ and read_vernac_file verbosely s =
  * with a new label to make vernac undoing easier. Also freeze state to speed up
  * backtracking. *)
 let eval_expr last =
-  vernac_com (States.with_heavy_rollback Vernacentries.interp) last;
+  vernac_com Vernacentries.interp last;
   Lib.add_frozen_state();
   Lib.mark_end_of_command()
 
-let eval_ctrl ast =
-  vernac_com Vernacentries.interp (Util.dummy_loc,ast)
-
 (* raw_do_vernac : Pcoq.Gram.parsable -> unit
  * vernac_step . parse_sentence *)
 let raw_do_vernac po = eval_expr (parse_sentence (po,None))
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 767c53063..d89e90d0c 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -22,7 +22,6 @@ exception End_of_input
 
 val just_parsing : bool ref
 val eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit
-val eval_ctrl : Vernacexpr.vernac_expr -> unit
 val raw_do_vernac : Pcoq.Gram.parsable -> unit
 
 (** Set XML hooks *)