Enforce a correct exception handling in declaration_hooks

This should finally get rid of the following class of bugs:
Qed fails, STM undoes to the beginning of the proof because the
exception is not annotated with the correct state, PG gets out of
sync because errors always refer to the last command in PGIP.

18 files changed, 68 insertions, 34 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 4b4a54a035..7895ddbf47 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -273,4 +273,4 @@ type raw_tactic_arg =
 type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
 type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
 
-type 'a declaration_hook = locality -> global_reference -> 'a
+type 'a declaration_hook = 'a Future.hook
diff --git a/lib/future.ml b/lib/future.ml
index 77386a1a9f..960363e252 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -91,6 +91,13 @@ let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None))
 let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ())))
 
 let fix_exn_of ck = let _, fix_exn, _ = get ck in fix_exn
+type 'a hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
+let mk_hook hook = hook
+let call_hook fix_exn hook l c =
+  try hook l c
+  with e when Errors.noncritical e ->
+    let e = Errors.push e in
+    raise (fix_exn e)
 
 let default_force () = raise NotReady
 let assignement ck = fun v ->
diff --git a/lib/future.mli b/lib/future.mli
index b4eced06a9..41f5e185c9 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -84,8 +84,18 @@ val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation
    the value is not just the 'a but also the global system state *)
 val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
 
-(* To get the fix_exn of a computation *)
+(* To get the fix_exn of a computation and build a Tacexpr.declaration_hook.
+ * When a future enters the environment a corresponding hook is run to perform
+ * some work.  If this fails, then its failure has to be annotated with the
+ * same state id that corresponds to the future computation end.  I.e. Qed
+ * is split into two parts, the lazy one (the future) and the eagher one
+ * (the hook), both performing some computations for the same state id. *)
 val fix_exn_of : 'a computation -> fix_exn
+type 'a hook
+val mk_hook :
+  (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a hook
+val call_hook :
+  fix_exn -> 'a hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
 
 (* Run remotely, returns the function to assign.  Optionally tekes a function
    that is called when forced.  The default one is to raise NotReady.
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f0c7b5a7f7..714192f530 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -988,7 +988,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
     (mk_equation_id f_id)
     (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
     (lemma_type, (*FIXME*) Univ.ContextSet.empty)
-    (fun _ _ -> ());
+    (Future.mk_hook (fun _ _ -> ()));
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
   Lemmas.save_proof (Vernacexpr.Proved(false,None))
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index a8876c75b1..65a2627070 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -290,7 +290,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
   let new_princ_name =
     next_ident_away_in_goal (Id.of_string "___________princ_________") []
   in
-  let hook = hook new_principle_type in
+  let hook = Future.mk_hook (hook new_principle_type) in
   begin
     Lemmas.start_proof
       new_princ_name
@@ -305,7 +305,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
     (* 	  let dur1 = System.time_difference tim1 tim2 in *)
     (* 	  Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
     (* 	end; *)
-    get_proof_clean true,Ephemeron.create hook
+    get_proof_clean true, Ephemeron.create hook
   end
 
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 70a892a3bb..8c8d7a667e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -352,7 +352,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
     | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
 	Command.do_definition fname (Decl_kinds.Global,(*FIXME*)false,Decl_kinds.Definition)
-	  bl None body (Some ret_type) (fun _ _ -> ())
+	  bl None body (Some ret_type) (Future.mk_hook (fun _ _ -> ()))
     | _ ->
 	Command.do_fixpoint Global false(*FIXME*) fixpoint_exprl
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 0d1e600ee6..b923260c24 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -147,6 +147,7 @@ let get_locality = function
 | Global -> false
 
 let save with_clean id const (locality,_,kind) hook =
+  let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
         let k = Kindops.logical_kind_of_goal_kind kind in
@@ -160,7 +161,7 @@ let save with_clean id const (locality,_,kind) hook =
 	(locality, ConstRef kn)
   in
   if with_clean then  Pfedit.delete_current_proof ();
-  Ephemeron.iter_opt hook (fun f -> f l r);
+  Ephemeron.iter_opt hook (fun f -> Future.call_hook fix_exn f l r);
   definition_message id
 
 
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 6e8b79a6be..3fafeadc1c 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -46,7 +46,7 @@ val const_of_id: Id.t -> constant
 val jmeq : unit -> Term.constr
 val jmeq_refl : unit -> Term.constr
 
-val save : bool -> Id.t ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
+val save : bool -> Id.t -> Entries.definition_entry  -> Decl_kinds.goal_kind ->
   unit Tacexpr.declaration_hook Ephemeron.key -> unit
 
 (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d5640798e2..9558923f6b 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1080,7 +1080,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
            (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty)
-           (fun _ _ -> ());
+           (Future.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
 	      (proving_tac i))));
@@ -1133,7 +1133,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem))
            (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty)
-           (fun _ _ -> ());
+           (Future.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
 	      (proving_tac i))));
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 4390143619..08d8ca3914 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1320,7 +1320,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
     na
     (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
     (gls_type, ctx)
-    hook;
+    (Future.mk_hook hook);
   if Indfun_common.is_strict_tcc  ()
   then
     ignore (by (Proofview.V82.tactic (tclIDTAC)))
@@ -1415,7 +1415,9 @@ let (com_eqn : int -> Id.t ->
     let f_constr = constr_of_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
     (Lemmas.start_proof eq_name (Global, false, Proof Lemma)
-       ~sign:(Environ.named_context_val env) (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty) (fun _ _ -> ());
+       ~sign:(Environ.named_context_val env)
+       (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty)
+       (Future.mk_hook (fun _ _ -> ()));
      ignore (by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
 	  (fun  x ->
@@ -1535,5 +1537,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       term_id
       using_lemmas
       (List.length res_vars)
-      ctx hook)
+      ctx (Future.mk_hook hook))
     ()
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 0668af2c50..493b874aed 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -168,6 +168,7 @@ let look_for_possibly_mutual_statements = function
 (* Saving a goal *)
 
 let save id const cstrs do_guard (locality,poly,kind) hook =
+  let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
   let const = adjust_guardness_conditions const do_guard in
   let k = Kindops.logical_kind_of_goal_kind kind in
   let l,r = match locality with
@@ -183,7 +184,7 @@ let save id const cstrs do_guard (locality,poly,kind) hook =
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
 	(locality, ConstRef kn) in
   definition_message id;
-  hook l r
+  Future.call_hook fix_exn hook l r
 
 let default_thm_id = Id.of_string "Unnamed_thm"
 
@@ -224,7 +225,7 @@ let save_remaining_recthms (locality,p,kind) body opaq i (id,((t_i,ctx_i),(_,imp
       let body_i = match kind_of_term body with
         | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
         | CoFix (0,decls) -> mkCoFix (i,decls)
-        | _ -> anomaly (Pp.str "Not a proof by induction") in
+        | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in
       match locality with
       | Discharge ->
           let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p 
@@ -285,7 +286,7 @@ let admit hook () =
       str "declared as an axiom.")
   in
   let () = assumption_message id in
-  hook Global (ConstRef kn)
+  Future.call_hook (fun exn -> exn) hook Global (ConstRef kn)
 
 (* Starting a goal *)
 
@@ -400,8 +401,8 @@ let start_proof_with_initialization kind recguard thms snl hook =
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
-	  hook strength ref) thms_data in
-      start_proof id kind t ?init_tac hook ~compute_guard:guard
+	  Future.call_hook (fun exn -> exn) hook strength ref) thms_data in
+      start_proof id kind t ?init_tac (Future.mk_hook hook) ~compute_guard:guard
 
 let start_proof_com kind thms hook =
   let env0 = Global.env () in
diff --git a/stm/stm.ml b/stm/stm.ml
index b6143df528..c708389908 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -763,7 +763,8 @@ end = struct
           !reach_known_state ~cache:`No eop;
           (* The original terminator, a hook, has not been saved in the .vi*)
           Proof_global.set_terminator
-            (Lemmas.standard_proof_terminator [] (fun _ _ -> ()));
+            (Lemmas.standard_proof_terminator []
+              (Future.mk_hook (fun _ _ -> ())));
           let proof = Proof_global.close_proof (fun x -> x) in
           vernac_interp eop ~proof
             { verbose = false; loc;
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 1e88456f36..1c98ec21dd 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1878,6 +1878,7 @@ let add_morphism_infer glob m n =
 	  declare_projection n instance_id (ConstRef cst)
 	| _ -> assert false
       in
+      let hook = Future.mk_hook hook in
 	Flags.silently
 	  (fun () ->
 	    Lemmas.start_proof instance_id kind (instance, ctx) hook;
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 9ca75d1737..1d85290511 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -304,6 +304,8 @@ let add_coercion_hook poly local ref =
   let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
   Flags.if_verbose msg_info msg
 
+let add_coercion_hook poly = Future.mk_hook (add_coercion_hook poly)
+
 let add_subclass_hook poly local ref =
   let stre = match local with
   | Local -> true
@@ -312,3 +314,5 @@ let add_subclass_hook poly local ref =
   in
   let cl = class_of_global ref in
   try_add_new_coercion_subclass cl stre poly
+
+let add_subclass_hook poly = Future.mk_hook (add_subclass_hook poly)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index b9c4a42943..5d1a0a43b6 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -294,6 +294,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 		  in obls, Some constr, typ
 		| None -> [||], None, termtype
 	      in
+              let hook = Future.mk_hook hook in
 	      let ctx = Evd.universe_context_set evm in
 		ignore (Obligations.add_definition id ?term:constr
 			typ ctx ~kind:(Global,poly,Instance) ~hook obls);
@@ -302,7 +303,8 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	      (Flags.silently 
 	       (fun () ->
 		Lemmas.start_proof id kind (termtype, Evd.universe_context_set evm)
-		(fun _ -> instance_hook k pri global imps ?hook);
+		(Future.mk_hook
+                  (fun _ -> instance_hook k pri global imps ?hook));
                  (* spiwack: I don't know what to do with the status here. *)
 		if not (Option.is_empty term) then 
 		  ignore (Pfedit.by (!refine_ref (evm, Option.get term)))
diff --git a/toplevel/command.ml b/toplevel/command.ml
index c1283fb1f4..b49fe40a09 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -163,7 +163,7 @@ let declare_definition ident (local, p, k) ce imps hook =
     VarRef ident
   | Discharge | Local | Global ->
     declare_global_definition ident ce local k imps in
-  hook local r
+  Future.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r
 
 let _ = Obligations.declare_definition_ref := declare_definition
 
@@ -183,10 +183,12 @@ let do_definition ident k bl red_option c ctypopt hook =
 	Obligations.eterm_obligations env ident evd 0 c typ
       in
       let ctx = Evd.universe_context_set evd in
-	ignore(Obligations.add_definition ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
+	ignore(Obligations.add_definition
+          ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
       ignore(declare_definition ident k ce imps
-        (fun l r -> hook l r;r))
+        (Future.mk_hook
+          (fun l r -> Future.call_hook (fun exn -> exn) hook l r;r)))
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
@@ -690,7 +692,7 @@ let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
 let declare_fix (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
   let ce = definition_entry ~types:t ~poly ~univs:ctx ~eff def in
-  declare_definition f kind ce imps (fun _ r -> r)
+  declare_definition f kind ce imps (Future.mk_hook (fun _ r -> r))
 
 let _ = Obligations.declare_fix_ref := declare_fix
 
@@ -898,6 +900,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 	  Impargs.declare_manual_implicits false gr [impls]
       in hook, recname, typ
   in
+  let hook = Future.mk_hook hook in
   let fullcoqc = Evarutil.nf_evar !evdref def in
   let fullctyp = Evarutil.nf_evar !evdref typ in
   Obligations.check_evars env !evdref;
@@ -991,7 +994,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
       Option.map (List.map Proofview.V82.tactic) init_tac
     in
     Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
-      (Some(false,indexes,init_tac)) thms None (fun _ _ -> ())
+      (Some(false,indexes,init_tac)) thms None (Future.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -1025,7 +1028,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns
       Option.map (List.map Proofview.V82.tactic) init_tac
     in
     Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
-      (Some(true,[],init_tac)) thms None (fun _ _ -> ())
+      (Some(true,[],init_tac)) thms None (Future.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index f8247c4ed6..00fc3e0ce1 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -535,7 +535,8 @@ let declare_definition prg =
     progmap_remove prg;
     !declare_definition_ref prg.prg_name 
       prg.prg_kind ce prg.prg_implicits
-      (fun l r -> prg.prg_hook l r; r)
+      (Future.mk_hook (fun l r ->
+         Future.call_hook (fun exn -> exn) prg.prg_hook l r; r))
 
 open Pp
 
@@ -606,7 +607,7 @@ let declare_mutual_definition l =
     Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
     let gr = List.hd kns in
     let kn = match gr with ConstRef kn -> kn | _ -> assert false in
-      first.prg_hook local gr;
+      Future.call_hook (fun exn -> exn) first.prg_hook local gr;
       List.iter progmap_remove l; kn
 
 let shrink_body c = 
@@ -815,7 +816,7 @@ let rec solve_obligation prg num tac =
           let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
             Lemmas.start_proof_univs obl.obl_name kind 
               (Universes.subst_opt_univs_constr prg.prg_subst obl.obl_type, ctx)
-              (fun (subst, ctx) strength gr ->
+              (fun (subst, ctx) -> Future.mk_hook (fun strength gr ->
 		let cst = match gr with ConstRef cst -> cst | _ -> assert false in
 		let obl =
 		  let transparent = evaluable_constant cst (Global.env ()) in
@@ -851,7 +852,7 @@ let rec solve_obligation prg num tac =
 		      let deps = dependencies obls num in
 			if not (Int.Set.is_empty deps) then
 			  ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps)
-		  | _ -> ());
+		  | _ -> ()));
 	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
 		     Printer.pr_constr_env (Global.env ()) obl.obl_type);
 	    ignore (Pfedit.by (snd (get_default_tactic ())));
@@ -976,7 +977,7 @@ let show_term n =
 	    ++ Printer.pr_constr_env (Global.env ()) prg.prg_body)
 
 let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
-    ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
+    ?(reduce=reduce) ?(hook=Future.mk_hook (fun _ _ -> ())) obls =
   let info = str (Id.to_string n) ++ str " has type-checked" in
   let prg = init_prog_info n term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
@@ -994,7 +995,7 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
 	| _ -> res)
 
 let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
-    ?(hook=fun _ _ -> ()) notations fixkind =
+    ?(hook=Future.mk_hook (fun _ _ -> ())) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 007ab52388..1fdf95c0f5 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -452,11 +452,12 @@ let start_proof_and_print k l hook =
   start_proof_com k l hook;
   print_subgoals ()
 
-let no_hook _ _ = ()
+let no_hook = Future.mk_hook (fun _ _ -> ())
 
 let vernac_definition_hook p = function
 | Coercion -> Class.add_coercion_hook p
-| CanonicalStructure -> fun _ -> Recordops.declare_canonical_structure
+| CanonicalStructure ->
+    Future.mk_hook (fun _ -> Recordops.declare_canonical_structure)
 | SubClass -> Class.add_subclass_hook p
 | _ -> no_hook