Proof_global: pass only 1 pstate when we don't want the proof stack

Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.

Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).

We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.

Behaviour should be similar modulo bugs, let's see what CI says.

1 files changed, 18 insertions, 13 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a6b088de0c..d47c12a7cb 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -410,7 +410,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
   with e when CErrors.noncritical e ->
     on_error names e
 
-let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
+let register_struct 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 
@@ -432,9 +432,9 @@ let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * V
 	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
        in
-       pstate, evd,List.rev rev_pconstants
+       None, evd,List.rev rev_pconstants
     | _ ->
-      let pstate = ComFixpoint.do_fixpoint ~ontop:pstate Global false fixpoint_exprl in
+      let pstate = ComFixpoint.do_fixpoint Global false fixpoint_exprl in
        let evd,rev_pconstants =
 	 List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
@@ -633,8 +633,8 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
   fixpoint_exprl_with_new_bl
   
 
-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 =
+let do_generate_principle pconstants on_error register_built interactive_proof
+    (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.pstate option =
   List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl;
   let pstate, _is_struct =
     match fixpoint_exprl with
@@ -661,7 +661,7 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive
 	  in
 	  if register_built
           then register_wf name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false
-          else pstate, false
+          else None, false
       |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,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 
@@ -685,7 +685,7 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive
 	  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
-          else pstate, true
+          else None, true
       | _ ->
           List.iter (function ((_na,ord,_args,_body,_type),_not) ->
 		       match ord with 
@@ -704,8 +704,8 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive
 	let is_rec = List.exists (is_rec fix_names) recdefs in
         let pstate,evd,pconstants =
 	  if register_built
-          then register_struct ~pstate is_rec fixpoint_exprl
-          else pstate, Evd.from_env (Global.env ()), pconstants
+          then register_struct is_rec fixpoint_exprl
+          else None, Evd.from_env (Global.env ()), pconstants
 	in
 	let evd = ref evd in 
 	generate_principle
@@ -839,9 +839,7 @@ let rec get_args b t : Constrexpr.local_binder_expr list *
     | _ -> [],b,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 make_graph env sigma (f_ref : GlobRef.t) =
   let c,c_body =
     match f_ref with
     | ConstRef c ->
@@ -902,11 +900,18 @@ let make_graph ~pstate (f_ref : GlobRef.t) =
                  [((CAst.make id,None),None,nal_tas,t,Some b),[]]
 	 in
          let mp = Constant.modpath c in
-         let pstate = do_generate_principle ~pstate [c,Univ.Instance.empty] error_error  false false expr_list in
+         let pstate = do_generate_principle [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;
          pstate)
 
+let make_graph ~ontop f_ref =
+  let pstate = Option.map Proof_global.get_current_pstate ontop in
+  let sigma, env = Option.cata Pfedit.get_current_context
+      (let e = Global.env () in Evd.from_env e, e) pstate in
+  Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop
+    (make_graph env sigma f_ref)
+
 let do_generate_principle = do_generate_principle [] warning_error true