Hack to correctly get ill-formed rec body exceptions even

when the environment is reset. Bug is due to the use of 
the imperative the_globrevtab when trying to pretty-print the terms
involved which may refer to the last defined obligation which is defined
in the exception's environment and not the global one anymore.
Bug reported by Francois Pottier.


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

2 files changed, 69 insertions, 57 deletions

diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index c1e168da17..071ffb2c5a 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -101,41 +101,52 @@ VERNAC COMMAND EXTEND Subtac
 [ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ]
   END
 
+let try_catch_exn f e =
+  try f e
+  with exn -> errorlabstrm "Program" (Cerrors.explain_exn exn)
+
+let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e
+let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e
+let try_solve_obligation e = try_catch_exn Subtac_obligations.try_solve_obligation e
+let try_solve_obligations e = try_catch_exn Subtac_obligations.try_solve_obligations e
+let solve_all_obligations e = try_catch_exn Subtac_obligations.solve_all_obligations e
+let admit_obligations e = try_catch_exn Subtac_obligations.admit_obligations e
+
 VERNAC COMMAND EXTEND Subtac_Obligations
-| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, Some t) ]
-| [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, None) ]
-| [ "Obligation" integer(num) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, None, Some t) ]      
-| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None, None) ]
-| [ "Next" "Obligation" "of" ident(name) ] -> [ Subtac_obligations.next_obligation (Some name) ]
-| [ "Next" "Obligation" ] -> [ Subtac_obligations.next_obligation None ]
+| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) ] -> [ subtac_obligation (num, Some name, Some t) ]
+| [ "Obligation" integer(num) "of" ident(name) ] -> [ subtac_obligation (num, Some name, None) ]
+| [ "Obligation" integer(num) ":" lconstr(t) ] -> [ subtac_obligation (num, None, Some t) ]      
+| [ "Obligation" integer(num) ] -> [ subtac_obligation (num, None, None) ]
+| [ "Next" "Obligation" "of" ident(name) ] -> [ next_obligation (Some name) ]
+| [ "Next" "Obligation" ] -> [ next_obligation None ]
 END
 
 VERNAC COMMAND EXTEND Subtac_Solve_Obligation
 | [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] -> 
-    [ Subtac_obligations.try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ]
+    [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ]
 | [ "Solve" "Obligation" integer(num) "using" tactic(t) ] -> 
-    [ Subtac_obligations.try_solve_obligation num None (Some (Tacinterp.interp t)) ]
+    [ try_solve_obligation num None (Some (Tacinterp.interp t)) ]
       END
 
 VERNAC COMMAND EXTEND Subtac_Solve_Obligations
 | [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> 
-    [ Subtac_obligations.try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ]
+    [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ]
 | [ "Solve" "Obligations" "using" tactic(t) ] -> 
-    [ Subtac_obligations.try_solve_obligations None (Some (Tacinterp.interp t)) ]
+    [ try_solve_obligations None (Some (Tacinterp.interp t)) ]
 | [ "Solve" "Obligations" ] -> 
-    [ Subtac_obligations.try_solve_obligations None None ]
+    [ try_solve_obligations None None ]
       END
 
 VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations
 | [ "Solve" "All" "Obligations" "using" tactic(t) ] -> 
-    [ Subtac_obligations.solve_all_obligations (Some (Tacinterp.interp t)) ]
+    [ solve_all_obligations (Some (Tacinterp.interp t)) ]
 | [ "Solve" "All" "Obligations" ] -> 
-    [ Subtac_obligations.solve_all_obligations None ]
+    [ solve_all_obligations None ]
       END
 
 VERNAC COMMAND EXTEND Subtac_Admit_Obligations
-| [ "Admit" "Obligations" "of" ident(name) ] -> [ Subtac_obligations.admit_obligations (Some name) ] 
-| [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ] 
+| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ] 
+| [ "Admit" "Obligations" ] -> [ admit_obligations None ] 
     END
 
 VERNAC COMMAND EXTEND Subtac_Set_Solver
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 74ac787064..c4efef11b1 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -1,4 +1,4 @@
-(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
+(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
 open Printf
 open Pp
 open Subtac_utils
@@ -347,23 +347,21 @@ let update_obls prg obls rem =
       if rem > 0 then Remain rem
       else (
 	match prg'.prg_deps with
-	    [] ->
-	      let kn = declare_definition prg' in
-		from_prg := ProgMap.remove prg.prg_name !from_prg;
-		Defined kn
-	  | l ->
-	      let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
-		if List.for_all (fun x -> obligations_solved x) progs then 
-		  (let kn = declare_mutual_definition progs in
-		     from_prg := List.fold_left
-		       (fun acc x -> 
-			 ProgMap.remove x.prg_name acc) !from_prg progs;
-		    Defined (ConstRef kn))
-		else Dependent);
-    in
-      update_state (!from_prg, !default_tactic_expr);
-      res
-	    
+	| [] ->
+	    let kn = declare_definition prg' in
+	      from_prg := ProgMap.remove prg.prg_name !from_prg;
+	      Defined kn
+	| l ->
+	    let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
+	      if List.for_all (fun x -> obligations_solved x) progs then 
+		(let kn = declare_mutual_definition progs in
+		   from_prg := List.fold_left
+		     (fun acc x -> 
+		       ProgMap.remove x.prg_name acc) !from_prg progs;
+		  Defined (ConstRef kn))
+	      else Dependent);
+    in update_state (!from_prg, !default_tactic_expr); res
+  
 let is_defined obls x = obls.(x).obl_body <> None
 
 let deps_remaining obls deps = 
@@ -421,7 +419,10 @@ let rec solve_obligation prg num =
 		in
 		let obls = Array.copy obls in
 		let _ = obls.(num) <- obl in
-		  match update_obls prg obls (pred rem) with
+		let res = try update_obls prg obls (pred rem) 
+		  with e -> pperror (Cerrors.explain_exn e) 
+		in
+		  match res with
 		  | Remain n when n > 0 ->
 		      if has_dependencies obls num then
 			ignore(auto_solve_obligations (Some prg.prg_name) None)
@@ -447,30 +448,30 @@ and subtac_obligation (user_num, name, typ) =
    
 and solve_obligation_by_tac prg obls i tac =
   let obl = obls.(i) in
-  match obl.obl_body with 
-      Some _ -> false
+    match obl.obl_body with 
+    | Some _ -> false
     | None -> 
-	(try
-	    if deps_remaining obls obl.obl_deps = [] then
-	     let obl = subst_deps_obl obls obl in
-	     let tac = 
-	       match tac with
-	       | Some t -> t
-	       | None -> 
-		   match obl.obl_tac with
-		   | Some t -> Tacinterp.interp t
-		   | None -> !default_tactic
-	     in
-	     let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
-	       obls.(i) <- declare_obligation obl t;
-	       true
-	    else false
-	  with
-	    | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
-	    | Stdpp.Exc_located(_, Refiner.FailError (_, s))
-	    | Refiner.FailError (_, s) ->
-		user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s)
-	    | e -> false)
+	try
+	  if deps_remaining obls obl.obl_deps = [] then
+	    let obl = subst_deps_obl obls obl in
+	    let tac = 
+	      match tac with
+	      | Some t -> t
+	      | None -> 
+		  match obl.obl_tac with
+		  | Some t -> Tacinterp.interp t
+		  | None -> !default_tactic
+	    in
+	    let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
+	      obls.(i) <- declare_obligation obl t;
+	      true
+	  else false
+	with
+	| Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
+	| Stdpp.Exc_located(_, Refiner.FailError (_, s))
+	| Refiner.FailError (_, s) ->
+	    user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s)
+	| e -> false
 
 and solve_prg_obligations prg tac = 
   let obls, rem = prg.prg_obligations in