[plugins] [funind] Adapt to removal of imperative proof state.

11 files changed, 283 insertions, 343 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 16f376931e..499005a4db 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -722,7 +722,7 @@ let build_proof
 					  (treat_new_case
 					     ptes_infos
                                              nb_instantiate_partial
-                                             (build_proof env sigma do_finalize)
+                                             (build_proof do_finalize)
 					     t
 					     dyn_infos)
 					  g'
@@ -733,7 +733,7 @@ let build_proof
 		    ]
 		    g
 	      in
-              build_proof env sigma do_finalize_t {dyn_infos with info = t} g
+              build_proof do_finalize_t {dyn_infos with info = t} g
           | Lambda(n,t,b) ->
 	      begin
 		match EConstr.kind sigma (pf_concl g) with
@@ -749,7 +749,7 @@ let build_proof
 			   in
 			   let new_infos = {dyn_infos with info = new_term} in
 			   let do_prove new_hyps =
-                             build_proof env sigma do_finalize
+                             build_proof do_finalize
 			       {new_infos with
 			       	  rec_hyps = new_hyps;
 				  nb_rec_hyps  = List.length new_hyps
@@ -762,7 +762,7 @@ let build_proof
 		      do_finalize dyn_infos g
 	      end
 	  | Cast(t,_,_) ->
-              build_proof env sigma do_finalize {dyn_infos with info = t} g
+              build_proof do_finalize {dyn_infos with info = t} g
           | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
 	      do_finalize dyn_infos g
 	  | App(_,_) ->
@@ -792,7 +792,7 @@ let build_proof
 		  | Lambda _ ->
 		      let new_term =
                         Reductionops.nf_beta env sigma dyn_infos.info in
-                      build_proof env sigma do_finalize {dyn_infos with info = new_term}
+                      build_proof do_finalize {dyn_infos with info = new_term}
 			g
 		  | LetIn _ ->
 		      let new_infos =
@@ -805,11 +805,11 @@ let build_proof
 			     h_reduce_with_zeta (Locusops.onHyp hyp_id))
 			   dyn_infos.rec_hyps;
 			 h_reduce_with_zeta Locusops.onConcl;
-                         build_proof env sigma do_finalize new_infos
+                         build_proof do_finalize new_infos
 			]
 			g
 		  | Cast(b,_,_) ->
-                      build_proof env sigma do_finalize {dyn_infos with info = b } g
+                      build_proof do_finalize {dyn_infos with info = b } g
 		  | Case _ | Fix _ | CoFix _ ->
 		      let new_finalize dyn_infos =
 			let new_infos =
@@ -819,7 +819,7 @@ let build_proof
 			in
                         build_proof_args env sigma do_finalize new_infos
 		      in
-                      build_proof env sigma new_finalize {dyn_infos  with info = f } g
+                      build_proof new_finalize {dyn_infos  with info = f } g
 	      end
 	  | Fix _ | CoFix _ ->
 	      user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet"))
@@ -839,12 +839,12 @@ let build_proof
 		   (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id))
 		   dyn_infos.rec_hyps;
 		 h_reduce_with_zeta Locusops.onConcl;
-                 build_proof env sigma do_finalize new_infos
+                 build_proof do_finalize new_infos
 		] g
 	  | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
-  and build_proof env sigma do_finalize dyn_infos g =
+  and build_proof do_finalize dyn_infos g =
 (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
-    observe_tac_stream (str "build_proof with " ++ pr_leconstr_env env sigma dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
+    observe_tac_stream (str "build_proof with " ++ pr_leconstr_env (pf_env g) (project g) dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
   and build_proof_args env sigma do_finalize dyn_infos (* f_args'  args *) :tactic =
     fun g ->
       let (f_args',args) = dyn_infos.info in
@@ -866,7 +866,7 @@ let build_proof
 		   {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args}
 		)
 	      in
-              build_proof env sigma do_finalize
+              build_proof do_finalize
 		{dyn_infos with info = arg }
 		g
       in
@@ -879,19 +879,7 @@ let build_proof
   in
     (* observe_tac "build_proof" *)
   fun g ->
-    let env = pf_env g in
-    let sigma = project g in
-    build_proof env sigma (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos g
-
-
-
-
-
-
-
-
-
-
+    build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos g
 
 
 (* Proof of principles from structural functions *)
@@ -1002,19 +990,18 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
       ]
   in
   (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *)
-  Lemmas.start_proof
+  let pstate = Lemmas.start_proof ~ontop:None
     (*i The next call to mk_equation_id is valid since we are constructing the lemma
       Ensures by: obvious
       i*)
     (mk_equation_id f_id)
     (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
     evd
-  lemma_type;
-  ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
-  Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)));
-  evd
-
-
+  lemma_type
+  in
+  let pstate,_ = Pfedit.by (Proofview.V82.tactic prove_replacement) pstate in
+  let pstate = Lemmas.save_proof ~pstate (Vernacexpr.(Proved(Proof_global.Transparent,None))) in
+  pstate, evd
 
 
 let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g =
@@ -1028,7 +1015,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 	Ensures by: obvious
 	i*)
       let equation_lemma_id = (mk_equation_id f_id) in
-      evd := generate_equation_lemma !evd all_funs  f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
+      evd := snd @@ generate_equation_lemma !evd all_funs  f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
       let _ =
 	match e with
 	  | Option.IsNone ->
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1217ba0eba..e9a2c285d0 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -308,31 +308,30 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in
   evd := sigma;
   let hook = Lemmas.mk_hook (hook new_principle_type) in
-  begin
-    Lemmas.start_proof
+  let pstate =
+    Lemmas.start_proof ~ontop:None
       new_princ_name
       (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
       !evd
       (EConstr.of_constr new_principle_type)
-  ;
-    (*       let _tim1 = System.get_time ()  in *)
-      let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in
-      ignore (Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)));
-    (*       let _tim2 =  System.get_time ()  in *)
-    (* 	begin *)
-    (* 	  let dur1 = System.time_difference tim1 tim2 in *)
-    (* 	  Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
-    (* 	end; *)
+  in
+  (*       let _tim1 = System.get_time ()  in *)
+  let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in
+  let pstate,_ = Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)) pstate in
+  (*       let _tim2 =  System.get_time ()  in *)
+  (* 	begin *)
+  (* 	  let dur1 = System.time_difference tim1 tim2 in *)
+  (* 	  Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
+  (* 	end; *)
 
-      let open Proof_global in
-      let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) in
-      match entries with
-      | [entry] ->
-        discard_current ();
-        (id,(entry,persistence)), hook
-      | _ ->
-        CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
-  end
+  let open Proof_global in
+  let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pstate in
+  match entries with
+  | [entry] ->
+    let pstate = discard_current pstate in
+    (id,(entry,persistence)), hook, pstate
+  | _ ->
+    CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
 
 let generate_functional_principle (evd: Evd.evar_map ref)
     interactive_proof
@@ -382,7 +381,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
       register_with_sort InProp;
       register_with_sort InSet
   in
-  let ((id,(entry,g_kind)),hook) =
+  let ((id,(entry,g_kind)),hook,pstate) =
     build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
     proof_tac hook
   in
@@ -390,25 +389,9 @@ let generate_functional_principle (evd: Evd.evar_map ref)
      Don't forget to close the goal if an error is raised !!!!
   *)
   let uctx = Evd.evar_universe_context sigma in
-  save false new_princ_name entry ~hook uctx g_kind
+  save new_princ_name entry ~hook uctx g_kind
   with e when CErrors.noncritical e ->
-    begin
-      begin
-	try
-	  let id = Proof_global.get_current_proof_name () in
-	  let s = Id.to_string id in
-	  let n = String.length "___________princ_________" in
-	  if String.length s >= n
-	  then if String.equal (String.sub s 0 n) "___________princ_________"
-	  then Proof_global.discard_current ()
-	  else ()
-	  else ()
-	with e when CErrors.noncritical e -> ()
-      end;
-      raise (Defining_principle e)
-    end
-(*   defined  () *)
-
+    raise (Defining_principle e)
 
 exception Not_Rec
 
@@ -537,7 +520,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
 	s::l_schemes -> s,l_schemes
       | _ -> anomaly (Pp.str "")
   in
-  let ((_,(const,_)),_) =
+  let ((_,(const,_)),_,pstate) =
     try
       build_functional_principle evd false
 	first_type
@@ -547,21 +530,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
 	(prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs)))
         (fun _ _ _ _ _ -> ())
     with e when CErrors.noncritical e ->
-       begin
-	 begin
-	   try
-	     let id = Proof_global.get_current_proof_name () in
-	     let s = Id.to_string id in
-	     let n = String.length "___________princ_________" in
-	     if String.length s >= n
-	     then if String.equal (String.sub s 0 n) "___________princ_________"
-		  then Proof_global.discard_current ()
-		  else ()
-	     else ()
-	   with e when CErrors.noncritical e -> ()
-	 end;
-	 raise (Defining_principle e)
-       end
+      raise (Defining_principle e)
 
   in
   incr i;
@@ -611,7 +580,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
 	   (* If we reach this point, the two principle are not mutually recursive
 	      We fall back to the previous method
 	   *)
-	     let ((_,(const,_)),_) =
+             let ((_,(const,_)),_,pstate) =
 	       build_functional_principle
 		 evd
 		 false
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 6f67ab4d8b..4e8cf80ed2 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -177,7 +177,7 @@ let () =
 
 (* TASSI: n'importe quoi ! *)
 VERNAC COMMAND EXTEND Function
-| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
+| ![ proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
     => { let hard = List.exists (function
            | _,((_,(_,(CMeasureRec _|CWfRec _)),_,_,_),_) -> true
            | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
@@ -223,37 +223,34 @@ let warning_error names e =
 }
 
 VERNAC COMMAND EXTEND NewFunctionalScheme
-| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
+| ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
    => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
    ->
-    {
+    { fun ~pstate ->
       begin
-	try
-	  Functional_principles_types.build_scheme fas
-	with Functional_principles_types.No_graph_found ->
-	  begin
-	    match fas with
-	      | (_,fun_name,_)::_ ->
-		  begin
-		    begin
-		      make_graph (Smartlocate.global_with_alias fun_name)
-		    end
-		  ;
-		    try Functional_principles_types.build_scheme fas
-		    with Functional_principles_types.No_graph_found ->
-		      CErrors.user_err Pp.(str "Cannot generate induction principle(s)")
-		      | e when CErrors.noncritical e ->
-			  let names = List.map (fun (_,na,_) -> na) fas in
-			  warning_error names e
-
-		  end
+        try
+          Functional_principles_types.build_scheme fas; pstate
+        with
+        | Functional_principles_types.No_graph_found ->
+          begin
+            match fas with
+            | (_,fun_name,_)::_ ->
+              begin
+                let pstate = make_graph ~pstate (Smartlocate.global_with_alias fun_name) in
+                try Functional_principles_types.build_scheme fas; pstate
+                with
+                | Functional_principles_types.No_graph_found ->
+                  CErrors.user_err Pp.(str "Cannot generate induction principle(s)")
+                | e when CErrors.noncritical e ->
+                  let names = List.map (fun (_,na,_) -> na) fas in
+                  warning_error names e; pstate
+              end
 	      | _ -> assert false (* we can only have non empty  list *)
-	  end
-	  | e when CErrors.noncritical e ->
-	      let names = List.map (fun (_,na,_) -> na) fas in
-	      warning_error names e
+          end
+        | e when CErrors.noncritical e ->
+          let names = List.map (fun (_,na,_) -> na) fas in
+          warning_error names e; pstate
       end
-
     }
 END
 (***** debug only ***)
@@ -266,5 +263,6 @@ END
 
 (***** debug only ***)
 VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
-| ["Generate" "graph" "for" reference(c)] -> { make_graph (Smartlocate.global_with_alias c) }
+| ![ proof ] ["Generate" "graph" "for" reference(c)] ->
+  { make_graph (Smartlocate.global_with_alias c) }
 END
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index f4807954a7..275b58f0aa 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -369,7 +369,7 @@ let add_pat_variables sigma pat typ env : Environ.env =
 	  let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in
 	  List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
   in
-  let new_env = add_pat_variables  env pat typ in
+  let new_env = add_pat_variables env pat typ in
   let res =
     fst (
       Context.Rel.fold_outside
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index b69ca7080c..a5c19f3217 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -410,11 +410,11 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
   with e when CErrors.noncritical e ->
     on_error names e
 
-let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
+let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
   match fixpoint_exprl with
     | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
-      ComDefinition.do_definition
+      ComDefinition.do_definition ~ontop:pstate
         ~program_mode:false
 	fname
         (Decl_kinds.Global,false,Decl_kinds.Definition) pl
@@ -432,9 +432,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
        in
-       evd,List.rev rev_pconstants
+       pstate, evd,List.rev rev_pconstants
     | _ ->
-       ComFixpoint.do_fixpoint Global false fixpoint_exprl;
+      let pstate = ComFixpoint.do_fixpoint ~ontop:pstate Global false fixpoint_exprl in
        let evd,rev_pconstants =
 	 List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
@@ -448,8 +448,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
        in
-       evd,List.rev rev_pconstants
-	   
+       pstate,evd,List.rev rev_pconstants
+
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
     is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
@@ -638,10 +638,10 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
   fixpoint_exprl_with_new_bl
   
 
-let do_generate_principle pconstants on_error register_built interactive_proof
-    (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) :unit =
+let do_generate_principle ~pstate pconstants on_error register_built interactive_proof
+    (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option =
   List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl;
-  let _is_struct =
+  let pstate, _is_struct =
     match fixpoint_exprl with
       | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] ->
           let (((({CAst.v=name},pl),_,args,types,body)),_)  as fixpoint_expr =
@@ -665,8 +665,8 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	      true
 	  in
 	  if register_built
-          then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook;
-	  false
+          then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, false
+          else pstate, false
       |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] ->
           let (((({CAst.v=name},_),_,args,types,body)),_)  as fixpoint_expr =
 	    match recompute_binder_list [fixpoint_expr] with 
@@ -689,8 +689,8 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	      true
 	  in
 	  if register_built
-          then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook;
-	  true
+          then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true
+          else pstate, true
       | _ ->
 	  List.iter (function ((_na,(_,ord),_args,_body,_type),_not) ->
 		       match ord with 
@@ -707,10 +707,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	(* ok all the expressions are structural *)
   	let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
 	let is_rec = List.exists (is_rec fix_names) recdefs in
-	let evd,pconstants =
+        let pstate,evd,pconstants =
 	  if register_built
-	  then register_struct is_rec fixpoint_exprl
-	  else (Evd.from_env (Global.env ()),pconstants)
+          then register_struct ~pstate is_rec fixpoint_exprl
+          else pstate, Evd.from_env (Global.env ()), pconstants
 	in
 	let evd = ref evd in 
 	generate_principle
@@ -723,10 +723,11 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	  recdefs
 	  interactive_proof
 	  (Functional_principles_proofs.prove_princ_for_struct evd interactive_proof);
-	if register_built then begin derive_inversion fix_names; end;
-	true; 
+          if register_built then
+            begin derive_inversion fix_names; end;
+          pstate, true
   in
-  ()
+  pstate
 
 let rec add_args id new_args = CAst.map (function
   | CRef (qid,_) as b ->
@@ -843,13 +844,14 @@ let rec get_args b t : Constrexpr.local_binder_expr list *
     | _ -> [],b,t
 
 
-let make_graph (f_ref : GlobRef.t) =
+let make_graph ~pstate (f_ref : GlobRef.t) =
+  let sigma, env = Option.cata Pfedit.get_current_context
+      (let e = Global.env () in Evd.from_env e, e) pstate in
   let c,c_body =
     match f_ref with
     | ConstRef c ->
       begin try c,Global.lookup_constant c
         with Not_found ->
-          let sigma, env = Pfedit.get_current_context () in
           raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) )
       end
     | _ -> raise (UserError (None, str "Not a function reference") )
@@ -857,8 +859,7 @@ let make_graph (f_ref : GlobRef.t) =
   (match Global.body_of_constant_body c_body with
      | None -> error "Cannot build a graph over an axiom!"
      | Some (body, _) ->
-	 let env = Global.env () in
-	 let sigma = Evd.from_env env in
+       let env = Global.env () in
 	 let extern_body,extern_type =
 	   with_full_print (fun () ->
 		(Constrextern.extern_constr false env sigma (EConstr.of_constr body),
@@ -902,12 +903,11 @@ let make_graph (f_ref : GlobRef.t) =
                  [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
 	 in
          let mp = Constant.modpath c in
-	 do_generate_principle [c,Univ.Instance.empty] error_error  false false expr_list;
+         let pstate = do_generate_principle ~pstate [c,Univ.Instance.empty] error_error  false false expr_list in
 	 (* We register the infos *)
 	 List.iter
            (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id)))
-	   expr_list)
+           expr_list;
+         pstate)
 
 let do_generate_principle = do_generate_principle [] warning_error true
-
-
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index f209fb19fd..acf85f539e 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -5,18 +5,16 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 
 val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 
-val do_generate_principle :  
-  bool -> 
-  (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> 
-  unit
-
+val do_generate_principle : pstate:Proof_global.t option ->
+  bool ->
+  (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
+  Proof_global.t option
 
-val functional_induction :  
+val functional_induction :
   bool ->
   EConstr.constr ->
   (EConstr.constr * EConstr.constr bindings) option ->
   Ltac_plugin.Tacexpr.or_and_intro_pattern option ->
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
-
-val make_graph : GlobRef.t -> unit
+val make_graph : pstate:Proof_global.t option -> GlobRef.t -> Proof_global.t option
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index e34323abf4..40f66ce5eb 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -129,7 +129,7 @@ let get_locality = function
 | Local -> true
 | Global -> false
 
-let save with_clean id const ?hook uctx (locality,_,kind) =
+let save id const ?hook uctx (locality,_,kind) =
   let fix_exn = Future.fix_exn_of const.const_entry_body in
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
@@ -143,7 +143,6 @@ let save with_clean id const ?hook uctx (locality,_,kind) =
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
 	(locality, ConstRef kn)
   in
-  if with_clean then Proof_global.discard_current ();
   Lemmas.call_hook ?hook ~fix_exn uctx [] l r;
   definition_message id
 
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 12facc5744..9670cf1fa7 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -43,8 +43,7 @@ val jmeq : unit -> EConstr.constr
 val jmeq_refl : unit -> EConstr.constr
 
 val save
-  :  bool
-  -> Id.t
+  :  Id.t
   -> Safe_typing.private_constants Entries.definition_entry
   -> ?hook:Lemmas.declaration_hook
   -> UState.t
@@ -78,15 +77,12 @@ val find_Function_infos : Constant.t -> function_info
 val find_Function_of_graph : inductive -> function_info
 (* WARNING: To be used just after the graph definition !!! *)
 val add_Function : bool -> Constant.t -> unit
-
 val update_Function : function_info -> unit
 
-
 (** debugging *)
 val pr_info : Environ.env -> Evd.evar_map -> function_info -> Pp.t
 val pr_table : Environ.env -> Evd.evar_map -> Pp.t
 
-
 (* val function_debug : bool ref  *)
 val do_observe : unit -> bool
 val do_rewrite_dependent : unit -> bool
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 37dbfec4c9..136848eb67 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -802,16 +802,16 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	     Ensures by: obvious
 	 i*)
 	 let lem_id = mk_correct_id f_id in
-	 let (typ,_) = lemmas_types_infos.(i) in 
-	 Lemmas.start_proof
+         let (typ,_) = lemmas_types_infos.(i) in
+         let pstate = Lemmas.start_proof ~ontop:None
 	   lem_id
            (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem)))
            !evd
-           typ;
-	 ignore (Pfedit.by
+           typ in
+         let pstate = fst @@ Pfedit.by
 		   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
-						      (proving_tac i))));
-         (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))));
+                                                      (proving_tac i))) pstate in
+         let _ = Lemmas.save_proof ~pstate (Vernacexpr.(Proved(Proof_global.Transparent,None))) in
 	 let finfo = find_Function_infos (fst f_as_constant) in
 	 (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
 	 let _,lem_cst_constr = Evd.fresh_global
@@ -865,13 +865,13 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	     Ensures by: obvious
 	   i*)
 	 let lem_id = mk_complete_id f_id in
-	 Lemmas.start_proof lem_id
+         let pstate = Lemmas.start_proof ~ontop:None lem_id
            (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
-         (fst lemmas_types_infos.(i));
-	 ignore (Pfedit.by
+         (fst lemmas_types_infos.(i)) in
+         let pstate = fst (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
-	      (proving_tac i)))) ;
-         (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))));
+              (proving_tac i))) pstate) in
+         let _pstate = Lemmas.save_proof ~pstate (Vernacexpr.(Proved(Proof_global.Transparent,None))) in
 	 let finfo = find_Function_infos (fst f_as_constant) in
 	 let _,lem_cst_constr = Evd.fresh_global
 				  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index e19741a4e9..43073fe07c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -72,7 +72,7 @@ let declare_fun f_id kind ?univs value =
   let ce = definition_entry ?univs value (*FIXME *) in
     ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
 
-let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Proof_global.Transparent,None)))
+let defined pstate = Lemmas.save_proof ~pstate (Vernacexpr.(Proved (Proof_global.Transparent,None)))
 
 let def_of_const t =
    match (Constr.kind t) with
@@ -228,6 +228,7 @@ let observe strm =
 
 let do_observe_tac s tac g = 
   let goal = Printer.pr_goal g in
+  let s = s (pf_env g) (project g) in
   let lmsg = (str "recdef : ") ++ s in 
   observe (s++fnl());
   Stack.push (lmsg,goal) debug_queue;
@@ -252,8 +253,8 @@ let observe_tclTHENLIST s tacl =
   then
     let rec aux n = function
       | [] -> tclIDTAC
-      | [tac] -> observe_tac (s ++ spc () ++ int n) tac
-      | tac::tacl -> observe_tac (s ++ spc () ++ int n) (tclTHEN tac (aux (succ n) tacl))
+      | [tac] -> observe_tac (fun env sigma -> s env sigma ++ spc () ++ int n) tac
+      | tac::tacl -> observe_tac (fun env sigma -> s env sigma ++ spc () ++ int n) (tclTHEN tac (aux (succ n) tacl))
     in
     aux 0 tacl
   else tclTHENLIST tacl
@@ -268,11 +269,11 @@ let tclUSER tac is_mes l g =
       | None -> tclIDTAC
       | Some l -> tclMAP (fun id -> tclTRY (Proofview.V82.of_tactic (clear [id]))) (List.rev l)
   in
-  observe_tclTHENLIST (str "tclUSER1")
+  observe_tclTHENLIST (fun _ _ -> str "tclUSER1")
     [
       clear_tac;
       if is_mes
-      then observe_tclTHENLIST (str "tclUSER2")
+      then observe_tclTHENLIST (fun _ _ -> str "tclUSER2")
         [
 	  Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
             (delayed_force Indfun_common.ltof_ref))]);
@@ -394,12 +395,12 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
     ) [] rev_context in 
     let rev_ids = pf_get_new_ids (List.rev ids) g in 
     let new_b = substl (List.map mkVar rev_ids) b in 
-    observe_tclTHENLIST (str "treat_case1") 
+    observe_tclTHENLIST (fun _ _ -> str "treat_case1")
       [
 	h_intros (List.rev rev_ids);
 	Proofview.V82.of_tactic (intro_using teq_id);
 	onLastHypId (fun heq -> 
-	  observe_tclTHENLIST (str "treat_case2")[
+          observe_tclTHENLIST (fun _ _ -> str "treat_case2")[
 	    Proofview.V82.of_tactic (clear to_intros);
 	    h_intros to_intros;
 	    (fun g' -> 
@@ -426,6 +427,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 
 let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
   let sigma = project g in
+  let env = pf_env g in
   match EConstr.kind sigma expr_info.info with 
     | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint")
     | Proj _ -> user_err Pp.(str "Function cannot treat projections")
@@ -441,18 +443,18 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
     | Prod _ -> 
       begin
 	try
-          check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
+          check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info g
 	with e when CErrors.noncritical e ->
-          user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
+          user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
       end
     | Lambda(n,t,b) ->
       begin
 	try
-          check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
+          check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info g
 	with e when CErrors.noncritical e ->
-          user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
+          user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
       end
     | Case(ci,t,a,l) -> 
       begin
@@ -480,8 +482,8 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
 	      jinfo.apP (f,args) expr_info continuation_tac in 
 	    travel_args jinfo
 	      expr_info.is_main_branch new_continuation_tac new_infos g
-          | Case _ ->  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
-          | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".")
+          | Case _ ->  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
+          | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env env sigma expr_info.info ++ Pp.str ".")
       end
     | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
     | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
@@ -503,10 +505,9 @@ and travel_args jinfo is_final continuation_tac infos =
       travel jinfo new_continuation_tac 
 	{infos with info=arg;is_final=false} 
 and travel jinfo continuation_tac expr_info =
-  fun g ->
   observe_tac
-    (str jinfo.message ++ Printer.pr_leconstr_env (pf_env g) (project g) expr_info.info)
-    (travel_aux jinfo continuation_tac expr_info) g
+    (fun env sigma -> str jinfo.message ++ Printer.pr_leconstr_env env sigma expr_info.info)
+    (travel_aux jinfo continuation_tac expr_info)
 
 (* Termination proof *) 
 
@@ -527,16 +528,16 @@ let rec prove_lt hyple g =
       in
       let y =
 	List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (mkVar h))))) in
-      observe_tclTHENLIST (str "prove_lt1")[
+      observe_tclTHENLIST (fun _ _ -> str "prove_lt1")[
 	Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
-	observe_tac (str "prove_lt") (prove_lt hyple)
+        observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple)
       ]
     with Not_found -> 
       (
 	(
-	  observe_tclTHENLIST (str "prove_lt2")[
+          observe_tclTHENLIST (fun _ _ -> str "prove_lt2")[
 	    Proofview.V82.of_tactic (apply (delayed_force lt_S_n));
-	    (observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption))
+            (observe_tac (fun _ _ -> str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption))
 	  ])
       )
   end
@@ -552,26 +553,26 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
       let h' = next_ident_away_in_goal (h'_id) ids in
       let ids = h'::ids in
       let def = next_ident_away_in_goal def_id ids in
-      observe_tclTHENLIST (str "destruct_bounds_aux1")[
+      observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux1")[
 	Proofview.V82.of_tactic (split (ImplicitBindings [s_max]));
 	Proofview.V82.of_tactic (intro_then
 	  (fun id -> 
             Proofview.V82.tactic begin
-	    observe_tac (str "destruct_bounds_aux") 
+            observe_tac (fun _ _ -> str "destruct_bounds_aux")
 	      (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id)))
 		 [
-		   observe_tclTHENLIST (str "")[Proofview.V82.of_tactic (intro_using h_id);
+                   observe_tclTHENLIST (fun _ _ -> str "")[Proofview.V82.of_tactic (intro_using h_id);
 			       Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])));
 			       Proofview.V82.of_tactic default_full_auto];
-		   observe_tclTHENLIST (str "destruct_bounds_aux2")[
-		     observe_tac (str "clearing k ") (Proofview.V82.of_tactic (clear [id]));
+                   observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux2")[
+                     observe_tac (fun _ _ -> str "clearing k ") (Proofview.V82.of_tactic (clear [id]));
 		     h_intros [k;h';def];
-		     observe_tac (str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl));
-		     observe_tac (str "unfold functional")
+                     observe_tac (fun _ _ -> str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl));
+                     observe_tac (fun _ _ -> str "unfold functional")
 		       (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
 					 evaluable_of_global_reference infos.func)]));
 		     (
-		       observe_tclTHENLIST (str "test")[
+                       observe_tclTHENLIST (fun _ _ -> str "test")[
 			 list_rewrite true
 			   (List.fold_right 
 			      (fun e acc -> (mkVar e,true)::acc)
@@ -582,16 +583,16 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 		      (*   (List.map (fun e -> (mkVar e,true)) infos.eqs) *)
 		      (*   ; *)
 			 
-			 (observe_tac (str "finishing") 
+                         (observe_tac (fun _ _ -> str "finishing")
 			    (tclORELSE
 			       (Proofview.V82.of_tactic intros_reflexivity)
-			       (observe_tac (str "calling prove_lt") (prove_lt hyple))))])
+                               (observe_tac (fun _ _ -> str "calling prove_lt") (prove_lt hyple))))])
 		   ]
 	      ]
 	      )end))
 	  ] g
       | (_,v_bound)::l -> 
-      observe_tclTHENLIST (str "destruct_bounds_aux3")[
+      observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux3")[
 	Proofview.V82.of_tactic (simplest_elim (mkVar v_bound));
 	Proofview.V82.of_tactic (clear [v_bound]);
 	tclDO 2 (Proofview.V82.of_tactic intro);
@@ -599,7 +600,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 	  (fun p_hyp -> 
 	    (onNthHypId 2 
 	       (fun p ->  
-		 observe_tclTHENLIST (str "destruct_bounds_aux4")[
+                 observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux4")[
 		   Proofview.V82.of_tactic (simplest_elim 
 		     (mkApp(delayed_force max_constr, [| bound; mkVar p|])));
 		   tclDO 3 (Proofview.V82.of_tactic intro);
@@ -623,32 +624,33 @@ let destruct_bounds infos =
 let terminate_app f_and_args expr_info continuation_tac infos = 
     if expr_info.is_final && expr_info.is_main_branch 
     then 
-      observe_tclTHENLIST (str "terminate_app1")[
+      observe_tclTHENLIST (fun _ _ -> str "terminate_app1")[
 	continuation_tac infos;
-	observe_tac (str "first split") 
+        observe_tac (fun _ _ -> str "first split")
 	  (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
-	observe_tac (str "destruct_bounds (1)") (destruct_bounds infos)
+        observe_tac (fun _ _ -> str "destruct_bounds (1)") (destruct_bounds infos)
       ]
     else continuation_tac infos
 
 let terminate_others _ expr_info continuation_tac infos = 
   if expr_info.is_final && expr_info.is_main_branch 
   then 
-    observe_tclTHENLIST (str "terminate_others")[
+    observe_tclTHENLIST (fun _ _ -> str "terminate_others")[
 	    continuation_tac infos;
-      observe_tac (str "first split") 
+      observe_tac (fun _ _ -> str "first split")
 	(Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
-      observe_tac (str "destruct_bounds") (destruct_bounds infos)
+      observe_tac (fun _ _ -> str "destruct_bounds") (destruct_bounds infos)
     ]
   else continuation_tac infos
 
 let terminate_letin (na,b,t,e) expr_info continuation_tac info g =
   let sigma = project g in
+  let env = pf_env g in
   let new_e = subst1 info.info e in 
   let new_forbidden = 
     let forbid = 
       try 
-        check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) b;
+        check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) b;
 	true
       with e when CErrors.noncritical e -> false
     in
@@ -693,7 +695,7 @@ let mkDestructEq :
   let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
            to_revert_constr in
     pf_typel new_hyps (fun _ ->
-    observe_tclTHENLIST (str "mkDestructEq")
+    observe_tclTHENLIST (fun _ _ -> str "mkDestructEq")
      [Proofview.V82.of_tactic (generalize new_hyps);
       (fun g2 ->
         let changefun patvars env sigma =
@@ -705,9 +707,10 @@ let mkDestructEq :
 
 let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
   let sigma = project g in
+  let env = pf_env g in
   let f_is_present =
     try
-      check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids) a;
+      check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) a;
       false
     with e when CErrors.noncritical e ->
       true
@@ -721,45 +724,46 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
   let destruct_tac,rev_to_thin_intro = 
     mkDestructEq [expr_info.rec_arg_id] a' g in 
   let to_thin_intro = List.rev rev_to_thin_intro in 
-  observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a')
+  observe_tac (fun _ _ -> str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a')
     (try
       (tclTHENS
 	 destruct_tac
-	 (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
+         (List.map_i (fun i e -> observe_tac (fun _ _ -> str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
 	 ))
     with 
       | UserError(Some "Refiner.thensn_tac3",_) 
       | UserError(Some "Refiner.tclFAIL_s",_) ->
-        (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info} )
+        (observe_tac (fun _ _ -> str "is computable " ++ Printer.pr_leconstr_env env sigma new_info.info) (next_step continuation_tac {new_info with info = Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info} )
 	))
     g
     
 let terminate_app_rec (f,args) expr_info continuation_tac _ g =
   let sigma = project g in
-  List.iter (check_not_nested (pf_env g) sigma (expr_info.f_id::expr_info.forbidden_ids))
+  let env = pf_env g in
+  List.iter (check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids))
     args;
   begin
     try 
       let v = List.assoc_f (List.equal (EConstr.eq_constr sigma)) args expr_info.args_assoc in
       let new_infos = {expr_info with info = v} in 
-      observe_tclTHENLIST (str "terminate_app_rec")[
+      observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec")[
 	continuation_tac new_infos;
 	if expr_info.is_final && expr_info.is_main_branch 
 	then
-	  observe_tclTHENLIST (str "terminate_app_rec1")[ 
-	    observe_tac (str "first split")
+          observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec1")[
+            observe_tac (fun _ _ -> str "first split")
 	      (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
-	    observe_tac (str "destruct_bounds (3)")
+            observe_tac (fun _ _ -> str "destruct_bounds (3)")
 	      (destruct_bounds new_infos)
 	  ]
 	else
 	  tclIDTAC			       
       ] g
     with Not_found -> 
-      observe_tac (str "terminate_app_rec not found") (tclTHENS
+      observe_tac (fun _ _ -> str "terminate_app_rec not found") (tclTHENS
 	(Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args))))
 	[		
-	  observe_tclTHENLIST (str "terminate_app_rec2")[
+          observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec2")[
 	    Proofview.V82.of_tactic (intro_using rec_res_id);
 	    Proofview.V82.of_tactic intro;
 	    onNthHypId 1 
@@ -772,14 +776,14 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ g =
 			 (v,v_bound)::expr_info.values_and_bounds; 
 		       args_assoc=(args,mkVar v)::expr_info.args_assoc
 		     } in
-		     observe_tclTHENLIST (str "terminate_app_rec3")[
+                     observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec3")[
 		       continuation_tac new_infos;
 		       if expr_info.is_final && expr_info.is_main_branch 
 		       then
-			 observe_tclTHENLIST (str "terminate_app_rec4")[ 
-			   observe_tac (str "first split") 
+                         observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec4")[
+                           observe_tac (fun _ _ -> str "first split")
 			     (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
-			   observe_tac (str "destruct_bounds (2)") 
+                           observe_tac (fun _ _ -> str "destruct_bounds (2)")
 			     (destruct_bounds new_infos)
 			 ]
 		       else
@@ -789,12 +793,12 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ g =
 		)
 	      )
 	  ];
-	  observe_tac (str "proving decreasing") (
+          observe_tac (fun _ _ -> str "proving decreasing") (
 	    tclTHENS (* proof of args < formal args *)
 	      (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv)))
 	      [ 
-		observe_tac (str "assumption") (Proofview.V82.of_tactic assumption);
-		observe_tclTHENLIST (str "terminate_app_rec5")
+                observe_tac (fun _ _ -> str "assumption") (Proofview.V82.of_tactic assumption);
+                observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec5")
 		  [
 		    tclTRY(list_rewrite true 
 			     (List.map 
@@ -830,7 +834,7 @@ let prove_terminate = travel terminate_info
 (* Equation proof *)
 
 let equation_case next_step (ci,a,t,l) expr_info continuation_tac infos = 
-  observe_tac (str "equation case") (terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos)
+  observe_tac (fun _ _ -> str "equation case") (terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos)
 
 let rec prove_le g = 
   let sigma = project g in
@@ -856,9 +860,9 @@ let rec prove_le g =
 	  let _,args = decompose_app sigma t in 
 	  List.hd (List.tl args)
 	in 
-	observe_tclTHENLIST (str "prove_le")[
+        observe_tclTHENLIST (fun _ _ -> str "prove_le")[
 	  Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|])));
-	  observe_tac (str "prove_le (rec)") (prove_le)
+          observe_tac (fun _ _ -> str "prove_le (rec)") (prove_le)
 	] 
       with Not_found -> tclFAIL 0 (mt())
     end;
@@ -868,8 +872,8 @@ let rec prove_le g =
 let rec make_rewrite_list expr_info max = function 
   | [] -> tclIDTAC
   | (_,p,hp)::l -> 
-    observe_tac (str "make_rewrite_list") (tclTHENS
-      (observe_tac (str "rewrite heq on " ++ Id.print p ) (
+    observe_tac (fun _ _ -> str "make_rewrite_list") (tclTHENS
+      (observe_tac (fun _ _ -> str "rewrite heq on " ++ Id.print p ) (
 	(fun g -> 
           let sigma = project g in
 	  let t_eq = compute_renamed_type g (mkVar hp) in
@@ -886,16 +890,16 @@ let rec make_rewrite_list expr_info max = function
                               CAst.make @@ (NamedHyp k, f_S max)]) false) g) )
       )
       [make_rewrite_list expr_info max l;
-       observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *)
+       observe_tclTHENLIST (fun _ _ -> str "make_rewrite_list")[ (* x < S max proof *)
 	 Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm));
-	 observe_tac (str "prove_le(2)") prove_le
+         observe_tac (fun _ _ -> str "prove_le(2)") prove_le
        ]
       ] )
 
 let make_rewrite expr_info l hp max = 
   tclTHENFIRST
-    (observe_tac (str "make_rewrite") (make_rewrite_list expr_info max l))
-    (observe_tac (str "make_rewrite") (tclTHENS
+    (observe_tac (fun _ _ -> str "make_rewrite") (make_rewrite_list expr_info max l))
+    (observe_tac (fun _ _ -> str "make_rewrite") (tclTHENS
        (fun g -> 
           let sigma = project g in
 	  let t_eq = compute_renamed_type g (mkVar hp) in
@@ -905,30 +909,30 @@ let make_rewrite expr_info l hp max =
             let def_na,_,_ = destProd sigma t in
             Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name
 	  in
-	 observe_tac (str "general_rewrite_bindings")
+         observe_tac (fun _ _ -> str "general_rewrite_bindings")
 	   (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
 	    (mkVar hp,
              ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr);
                               CAst.make @@ (NamedHyp k, f_S (f_S max))]) false)) g)
-       [observe_tac(str "make_rewrite finalize") (
+       [observe_tac(fun _ _ -> str "make_rewrite finalize") (
 	 (* tclORELSE( h_reflexivity) *)
-	 (observe_tclTHENLIST (str "make_rewrite")[
+         (observe_tclTHENLIST (fun _ _ -> str "make_rewrite")[
 	   Proofview.V82.of_tactic (simpl_iter Locusops.onConcl);
-	   observe_tac (str "unfold functional")
+           observe_tac (fun _ _ -> str "unfold functional")
 	     (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
 			       evaluable_of_global_reference expr_info.func)]));
 	   
 	   (list_rewrite true 
 	      (List.map (fun e -> mkVar e,true) expr_info.eqs));
-	   (observe_tac (str "h_reflexivity")
+           (observe_tac (fun _ _ -> str "h_reflexivity")
 			(Proofview.V82.of_tactic intros_reflexivity)
 	   )
 	    ]))
        ;
-	 observe_tclTHENLIST (str "make_rewrite1")[ (* x < S (S max) proof *)
+         observe_tclTHENLIST (fun _ _ -> str "make_rewrite1")[ (* x < S (S max) proof *)
 	 Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_lt_SS)));
-	 observe_tac (str "prove_le (3)") prove_le
+         observe_tac (fun _ _ -> str "prove_le (3)") prove_le
 	 ]
        ])  
     )
@@ -937,7 +941,7 @@ let rec compute_max rew_tac max l =
   match l with 
     | [] -> rew_tac max
     | (_,p,_)::l -> 
-      observe_tclTHENLIST (str "compute_max")[
+      observe_tclTHENLIST (fun _ _ -> str "compute_max")[
 	Proofview.V82.of_tactic (simplest_elim 
 	  (mkApp(delayed_force max_constr, [| max; mkVar p|])));
 	tclDO 3 (Proofview.V82.of_tactic intro);
@@ -954,17 +958,17 @@ let rec destruct_hex expr_info acc l =
 	match List.rev acc with 
 	  | [] -> tclIDTAC 
 	  | (_,p,hp)::tl  -> 
-	    observe_tac (str "compute max ") (compute_max (make_rewrite expr_info tl hp) (mkVar p) tl)
+            observe_tac (fun _ _ -> str "compute max ") (compute_max (make_rewrite expr_info tl hp) (mkVar p) tl)
       end
     | (v,hex)::l -> 
-      observe_tclTHENLIST (str "destruct_hex")[
+      observe_tclTHENLIST (fun _ _ -> str "destruct_hex")[
 	Proofview.V82.of_tactic (simplest_case (mkVar hex));
 	Proofview.V82.of_tactic (clear [hex]);
 	tclDO 2 (Proofview.V82.of_tactic intro);
 	onNthHypId 1 (fun hp -> 
 	  onNthHypId 2 (fun p -> 
 	    observe_tac 
-	      (str "destruct_hex after " ++ Id.print hp ++ spc () ++ Id.print p)
+              (fun _ _ -> str "destruct_hex after " ++ Id.print hp ++ spc () ++ Id.print p)
 	      (destruct_hex expr_info ((v,p,hp)::acc) l)
 	  )
 	)
@@ -972,7 +976,7 @@ let rec destruct_hex expr_info acc l =
 	
 let rec intros_values_eq expr_info acc = 
   tclORELSE(
-    observe_tclTHENLIST (str "intros_values_eq")[
+    observe_tclTHENLIST (fun _ _ -> str "intros_values_eq")[
       tclDO 2 (Proofview.V82.of_tactic intro);
       onNthHypId 1 (fun hex -> 
 	(onNthHypId 2 (fun v -> intros_values_eq expr_info ((v,hex)::acc)))
@@ -983,23 +987,17 @@ let rec intros_values_eq expr_info acc =
     ))
 
 let equation_others _ expr_info continuation_tac infos = 
-  fun g ->
-  let env = pf_env g in
-  let sigma = project g in
   if expr_info.is_final && expr_info.is_main_branch 
   then
-    observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr_env env sigma expr_info.info)
+    observe_tac (fun env sigma -> str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr_env env sigma expr_info.info)
 		(tclTHEN 
       (continuation_tac infos) 
-      (fun g ->
-       let env = pf_env g in
-       let sigma = project g in
-       observe_tac (str "intros_values_eq equation_others "  ++ Printer.pr_leconstr_env env sigma expr_info.info) (intros_values_eq expr_info []) g)) g
-  else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr_env env sigma expr_info.info) (continuation_tac infos) g
+      (observe_tac (fun env sigma -> str "intros_values_eq equation_others "  ++ Printer.pr_leconstr_env env sigma expr_info.info) (intros_values_eq expr_info [])))
+  else observe_tac (fun env sigma -> str "equation_others (cont_tac) " ++ Printer.pr_leconstr_env env sigma expr_info.info) (continuation_tac infos)
 
 let equation_app f_and_args expr_info continuation_tac infos = 
     if expr_info.is_final && expr_info.is_main_branch 
-    then ((observe_tac (str "intros_values_eq equation_app") (intros_values_eq expr_info [])))
+    then ((observe_tac (fun _ _ -> str "intros_values_eq equation_app") (intros_values_eq expr_info [])))
     else continuation_tac infos
 	    
 let equation_app_rec (f,args) expr_info continuation_tac info g = 
@@ -1008,19 +1006,19 @@ let equation_app_rec (f,args) expr_info continuation_tac info g =
     try
       let v = List.assoc_f (List.equal (EConstr.eq_constr sigma)) args expr_info.args_assoc in
       let new_infos = {expr_info with info = v} in
-      observe_tac (str "app_rec found") (continuation_tac new_infos) g
+      observe_tac (fun _ _ -> str "app_rec found") (continuation_tac new_infos) g
     with Not_found ->
       if expr_info.is_final && expr_info.is_main_branch 
       then 
-	observe_tclTHENLIST (str "equation_app_rec")
+        observe_tclTHENLIST (fun _ _ -> str "equation_app_rec")
 	  [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
 	    continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc};
-	    observe_tac (str "app_rec intros_values_eq") (intros_values_eq expr_info [])
+            observe_tac (fun _ _ -> str "app_rec intros_values_eq") (intros_values_eq expr_info [])
 	  ] g
       else 
-	observe_tclTHENLIST (str "equation_app_rec1")[
+        observe_tclTHENLIST (fun _ _ -> str "equation_app_rec1")[
   	  Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
-	  observe_tac (str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc})
+          observe_tac (fun _ _ -> str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc})
 	] g
   end
 
@@ -1104,7 +1102,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 	(h_intros args_id)
 	(tclTHENS
 	   (observe_tac
-	      (str "first assert")
+              (fun _ _ -> str "first assert")
 	      (Proofview.V82.of_tactic (assert_before
 		 (Name wf_rec_arg)
 		 (mkApp (delayed_force acc_rel,
@@ -1116,7 +1114,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 	     (* accesibility proof *)
 	     tclTHENS
 	       (observe_tac
-		  (str "second assert")
+                  (fun _ _ -> str "second assert")
 		  (Proofview.V82.of_tactic (assert_before
 		     (Name wf_thm)
 		     (mkApp (delayed_force well_founded,[|input_type;relation|]))
@@ -1124,26 +1122,26 @@ let termination_proof_header is_mes input_type ids args_id relation
 	       )
 	       [
 		 (* interactive proof that the relation is well_founded *)
-		 observe_tac (str "wf_tac") (wf_tac is_mes (Some args_id));
+                 observe_tac (fun _ _ -> str "wf_tac") (wf_tac is_mes (Some args_id));
 		 (* this gives the accessibility argument *)
 		 observe_tac
-		   (str "apply wf_thm")
+                   (fun _ _ -> str "apply wf_thm")
 		   (Proofview.V82.of_tactic (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|])))
 		   )
 	       ]
 	     ;
 	     (* rest of the proof *)
-	     observe_tclTHENLIST (str "rest of proof")
-	       [observe_tac (str "generalize")
+             observe_tclTHENLIST (fun _ _ -> str "rest of proof")
+               [observe_tac (fun _ _ -> str "generalize")
 		  (onNLastHypsId (nargs+1)
 		     (tclMAP (fun id ->
 			tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id])))
 		     ))
 	       ;
-                observe_tac (str "fix") (Proofview.V82.of_tactic (fix hrec (nargs+1)));
+                observe_tac (fun _ _ -> str "fix") (Proofview.V82.of_tactic (fix hrec (nargs+1)));
 		h_intros args_id;
 		Proofview.V82.of_tactic (Simple.intro wf_rec_arg);
-		observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv)
+                observe_tac (fun _ _ -> str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv)
 	       ]
 	   ]
 	) g
@@ -1222,8 +1220,8 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
 	g
   end
 
-let get_current_subgoals_types () =
-  let p = Proof_global.give_me_the_proof () in
+let get_current_subgoals_types pstate =
+  let p = Proof_global.give_me_the_proof pstate in
   let sgs,_,_,_,sigma = Proof.proof p in
   sigma, List.map (Goal.V82.abstract_type sigma) sgs
 
@@ -1283,8 +1281,8 @@ let clear_goals sigma =
   List.map clear_goal
 
 
-let build_new_goal_type () =
-  let sigma, sub_gls_types = get_current_subgoals_types () in
+let build_new_goal_type pstate =
+  let sigma, sub_gls_types = get_current_subgoals_types pstate in
   (* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
   let sub_gls_types = clear_goals sigma sub_gls_types in
   (* Pp.msgnl (str "sub_gls_types2 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
@@ -1299,9 +1297,9 @@ let is_opaque_constant c =
     | Declarations.Def _ -> Proof_global.Transparent
     | Declarations.Primitive _ -> Proof_global.Opaque
 
-let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal)   =
+let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal)   =
   (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
-  let current_proof_name = Proof_global.get_current_proof_name () in
+  let current_proof_name = Proof_global.get_current_proof_name pstate in
   let name = match goal_name with
     | Some s -> s
     | None   ->
@@ -1325,11 +1323,10 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
     let lid = ref [] in
     let h_num = ref (-1) in
     let env = Global.env () in
-    Proof_global.discard_all ();
-    build_proof (Evd.from_env env)
+    let pstate = build_proof env (Evd.from_env env)
       (  fun gls ->
 	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
-	   observe_tclTHENLIST (str "")
+           observe_tclTHENLIST (fun _ _ -> str "")
 	     [
 	       Proofview.V82.of_tactic (generalize [lemma]);
 	       Proofview.V82.of_tactic (Simple.intro hid);
@@ -1353,7 +1350,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	       Proofview.V82.of_tactic (Auto.h_auto None [] (Some []))  g
 	   | _ ->
 	       incr h_num;
-	       (observe_tac (str "finishing using")
+               (observe_tac (fun _ _ -> str "finishing using")
 		  (
 		    tclCOMPLETE(
 		      tclFIRST[
@@ -1369,20 +1366,19 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 		  )
 	       )
       		 g)
-;
-    Lemmas.save_proof (Vernacexpr.Proved(opacity,None));
+    in
+    let _pstate = Lemmas.save_proof ~pstate (Vernacexpr.Proved(opacity,None)) in
+    ()
   in
-  Lemmas.start_proof
+  let pstate = Lemmas.start_proof ~ontop:(Some pstate)
     na
     (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
-    sigma gls_type
-    ~hook:(Lemmas.mk_hook hook);
-  if Indfun_common.is_strict_tcc  ()
+    sigma gls_type ~hook:(Lemmas.mk_hook hook) in
+  let pstate = if Indfun_common.is_strict_tcc  ()
   then
-    ignore (by (Proofview.V82.tactic (tclIDTAC)))
+    fst @@ by (Proofview.V82.tactic (tclIDTAC)) pstate
   else 
-    begin
-      ignore (by (Proofview.V82.tactic begin
+    fst @@ by (Proofview.V82.tactic begin
 	fun g ->
 	  tclTHEN
 	    (decompose_and_tac)
@@ -1398,12 +1394,12 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	 	     )
 	 	     using_lemmas)
 	       ) tclIDTAC)
-	    g end))
-    end;
+            g end) pstate
+  in
   try
-    ignore (by (Proofview.V82.tactic tclIDTAC)); (* raises UserError _ if the proof is complete *)
+    Some (fst @@ by (Proofview.V82.tactic tclIDTAC) pstate) (* raises UserError _ if the proof is complete *)
   with UserError _ ->
-    defined ()
+    defined pstate
 
 
 
@@ -1418,32 +1414,26 @@ let com_terminate
     thm_name using_lemmas
     nb_args ctx
     hook =
-  let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
-    let evd, env = Pfedit.get_current_context () in (* XXX *)
-    Lemmas.start_proof thm_name
+  let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
+    let pstate = Lemmas.start_proof ~ontop:None thm_name
       (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
-      ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook;
-
-    ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)));
-    ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
-    				   input_type relation rec_arg_num ))))
+      ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook in
+    let pstate = fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) pstate in
+    fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
+                                   input_type relation rec_arg_num ))) pstate
   in
-  start_proof ctx tclIDTAC tclIDTAC;
+  let pstate = start_proof Global.(env ()) ctx tclIDTAC tclIDTAC in
   try
-    let sigma, new_goal_type = build_new_goal_type () in
+    let sigma, new_goal_type = build_new_goal_type pstate in
     let sigma = Evd.from_ctx (Evd.evar_universe_context sigma) in
-    open_new_goal start_proof sigma
+    open_new_goal pstate start_proof sigma
       using_lemmas tcc_lemma_ref
       (Some tcc_lemma_name)
-      (new_goal_type);
+      (new_goal_type)
   with EmptySubgoals ->
     (* a non recursive function declared with measure ! *)
     tcc_lemma_ref := Not_needed;
-    defined ()
-
-
-
-
+    defined pstate
 
 let start_equation (f:GlobRef.t) (term_f:GlobRef.t)
   (cont_tactic:Id.t list -> tactic) g =
@@ -1453,13 +1443,13 @@ let start_equation (f:GlobRef.t) (term_f:GlobRef.t)
   let terminate_constr = EConstr.of_constr terminate_constr in
   let nargs = nb_prod (project g) (EConstr.of_constr (type_of_const sigma terminate_constr)) in
   let x = n_x_id ids nargs in
-  observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [
+  observe_tac (fun _ _ -> str "start_equation") (observe_tclTHENLIST (fun _ _ -> str "start_equation") [
     h_intros x;
     Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]);
-    observe_tac (str "simplest_case")
+    observe_tac (fun _ _ -> str "simplest_case")
       (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr,
                              Array.of_list (List.map mkVar x)))));
-    observe_tac (str "prove_eq") (cont_tactic x)]) g;;
+    observe_tac (fun _ _ -> str "prove_eq") (cont_tactic x)]) g;;
 
 let (com_eqn : int -> Id.t ->
        GlobRef.t -> GlobRef.t -> GlobRef.t
@@ -1471,15 +1461,17 @@ let (com_eqn : int -> Id.t ->
 	| ConstRef c -> is_opaque_constant c
 	| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
     in
-    let evd, env = Pfedit.get_current_context () in (* XXX *)
-    let evd = Evd.from_ctx (Evd.evar_universe_context evd) in
+    (* let evd, env = Pfedit.get_current_context () in *)
+    let env = Global.env () in
+    (* let evd = Evd.from_ctx (Evd.evar_universe_context evd) in *)
+    let evd = Evd.from_env env in
     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)
+    let pstate = Lemmas.start_proof ~ontop:None eq_name (Global, false, Proof Lemma)
        ~sign:(Environ.named_context_val env)
        evd
-       (EConstr.of_constr equation_lemma_type);
-     ignore (by
+       (EConstr.of_constr equation_lemma_type) in
+    let pstate = fst @@ by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
 	  (fun  x ->
 	     prove_eq (fun _ -> tclIDTAC)
@@ -1506,15 +1498,16 @@ let (com_eqn : int -> Id.t ->
 		ih = Id.of_string "______";
 	       }
 	  )
-       ))); 
+       )) pstate in
      (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
 (*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
-     Flags.silently (fun () -> Lemmas.save_proof (Vernacexpr.Proved(opacity,None))) () ; 
-(*      Pp.msgnl (str "eqn finished"); *)
-    );;
+    let _ = Flags.silently (fun () -> Lemmas.save_proof ~pstate (Vernacexpr.Proved(opacity,None))) () in
+    ()
+(*      Pp.msgnl (fun _ _ -> str "eqn finished"); *)
+
 
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
-    generate_induction_principle using_lemmas : unit =
+    generate_induction_principle using_lemmas : Proof_global.t option =
   let open Term in
   let open Constr in
   let open CVars in
@@ -1529,15 +1522,15 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in
   let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in
   let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in
- (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
+ (* Pp.msgnl (fun _ _ -> str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
   let res_vars,eq' = decompose_prod equation_lemma_type in
   let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in
   let eq' = Reductionops.nf_zeta env_eq' evd (EConstr.of_constr eq') in
   let eq' = EConstr.Unsafe.to_constr eq' in
   let res =
-(*     Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
-(*     Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)
-(*     Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *)
+(*     Pp.msgnl (fun _ _ -> str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
+(*     Pp.msgnl (fun _ _ -> str "rec_arg_num := " ++ str (fun _ _ -> string_of_int rec_arg_num)); *)
+(*     Pp.msgnl (fun _ _ -> str "eq' := " ++ str (fun _ _ -> string_of_int rec_arg_num)); *)
     match Constr.kind eq' with
       | App(e,[|_;_;eq_fix|]) ->
           mkLambda (make_annot (Name function_name) Sorts.Relevant,function_type,subst_var function_name (compose_lam res_vars  eq_fix))
@@ -1562,7 +1555,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let evd = Evd.from_ctx evuctx in
   let tcc_lemma_name = add_suffix function_name "_tcc" in
   let tcc_lemma_constr = ref Undefined in
-  (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
+  (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
   let hook _ _ _ _ =
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
@@ -1601,14 +1594,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   in
   (* XXX STATE Why do we need this... why is the toplevel protection not enought *)
   funind_purify (fun () ->
-    com_terminate
-      tcc_lemma_name
-      tcc_lemma_constr
-      is_mes functional_ref
-      (EConstr.of_constr rec_arg_type)
-      relation rec_arg_num
-      term_id
-      using_lemmas
-      (List.length res_vars)
-      evd (Lemmas.mk_hook hook))
-    ()
+      let pstate = com_terminate
+          tcc_lemma_name
+          tcc_lemma_constr
+          is_mes functional_ref
+          (EConstr.of_constr rec_arg_type)
+          relation rec_arg_num
+          term_id
+          using_lemmas
+          (List.length res_vars)
+          evd (Lemmas.mk_hook hook)
+      in pstate) ()
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 549f1fc0e4..a006c2c354 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -14,6 +14,6 @@ bool ->
            int -> Constrexpr.constr_expr -> (pconstant ->
             Indfun_common.tcc_lemma_value ref ->
             pconstant ->
-            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> unit
+            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option