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.

8 files changed, 56 insertions, 51 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f2b9ba2ec6..e38ea992ab 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -990,7 +990,7 @@ 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); *)
-  let pstate = Lemmas.start_proof ~ontop:None
+  let pstate = Lemmas.start_proof
     (*i The next call to mk_equation_id is valid since we are constructing the lemma
       Ensures by: obvious
       i*)
@@ -1000,8 +1000,9 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   lemma_type
   in
   let pstate,_ = Pfedit.by (Proofview.V82.tactic prove_replacement) pstate in
-  let pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in
-  pstate, evd
+  let ontop = Proof_global.push ~ontop:None pstate in
+  ignore(Lemmas.save_proof_proved ?proof:None ~ontop ~opaque:Proof_global.Transparent ~idopt:None);
+  evd
 
 
 let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g =
@@ -1015,7 +1016,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 := snd @@ generate_equation_lemma !evd all_funs  f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
+      evd := 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 2c107d39d9..7b26cb0c74 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -309,7 +309,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   evd := sigma;
   let hook = Lemmas.mk_hook (hook new_principle_type) in
   let pstate =
-    Lemmas.start_proof ~ontop:None
+    Lemmas.start_proof
       new_princ_name
       (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
       !evd
@@ -328,8 +328,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   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
+    (id,(entry,persistence)), hook
   | _ ->
     CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
 
@@ -381,7 +380,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,pstate) =
+  let ((id,(entry,g_kind)),hook) =
     build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
     proof_tac hook
   in
@@ -520,7 +519,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,_)),_,pstate) =
+  let ((_,(const,_)),_) =
     try
       build_functional_principle evd false
 	first_type
@@ -580,7 +579,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,_)),_,pstate) =
+             let ((_,(const,_)),_) =
 	       build_functional_principle
 		 evd
 		 false
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index dbfc0fc91d..b8db3dc5ce 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -190,7 +190,9 @@ VERNAC COMMAND EXTEND Function
          | Vernacextend.VtSideff ids, _ when hard ->
              Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
          | x -> x }
-    -> { do_generate_principle false (List.map snd recsl) }
+    -> { fun ~pstate:ontop ->
+      let pstate = do_generate_principle false (List.map snd recsl) in
+      Proof_global.maybe_push ~ontop pstate}
 END
 
 {
@@ -228,30 +230,30 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
 | ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
    => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
    ->
-    { fun ~pstate ->
+    { fun ~pstate:ontop ->
       begin
         try
-          Functional_principles_types.build_scheme fas; pstate
+          Functional_principles_types.build_scheme fas; ontop
         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
+                let ontop = make_graph ~ontop (Smartlocate.global_with_alias fun_name) in
+                try Functional_principles_types.build_scheme fas; ontop
                 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
+                  warning_error names e; ontop
               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; pstate
+          warning_error names e; ontop
       end
     }
 END
@@ -266,5 +268,5 @@ END
 (***** debug only ***)
 VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
 | ![ proof ] ["Generate" "graph" "for" reference(c)] ->
-  { make_graph (Smartlocate.global_with_alias c) }
+  { fun ~pstate:ontop -> make_graph ~ontop (Smartlocate.global_with_alias c) }
 END
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
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index acf85f539e..cf4ef23d1a 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -5,10 +5,10 @@ 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 : pstate:Proof_global.t option ->
+val do_generate_principle :
   bool ->
   (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
-  Proof_global.t option
+  Proof_global.pstate option
 
 val functional_induction :
   bool ->
@@ -17,4 +17,4 @@ val functional_induction :
   Ltac_plugin.Tacexpr.or_and_intro_pattern option ->
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
-val make_graph : pstate:Proof_global.t option -> GlobRef.t -> Proof_global.t option
+val make_graph : ontop:Proof_global.t option -> GlobRef.t -> Proof_global.t option
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2a0140f02c..03568fc6c7 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -803,7 +803,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	 i*)
 	 let lem_id = mk_correct_id f_id in
          let (typ,_) = lemmas_types_infos.(i) in
-         let pstate = Lemmas.start_proof ~ontop:None
+         let pstate = Lemmas.start_proof
 	   lem_id
            (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem)))
            !evd
@@ -811,7 +811,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let pstate = fst @@ Pfedit.by
 		   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
                                                       (proving_tac i))) pstate in
-         let _ = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in
+         let () = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt: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
-         let pstate = Lemmas.start_proof ~ontop:None lem_id
+         let pstate = Lemmas.start_proof lem_id
            (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
          (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))) pstate) in
-         let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in
+         let () = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt: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 de1b592337..b4d0f092d8 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 pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None
+let defined pstate = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None
 
 let def_of_const t =
    match (Constr.kind t) with
@@ -1367,10 +1367,9 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type
 	       )
       		 g)
     in
-    let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None in
-    ()
+    Lemmas.save_pstate_proved ~pstate ~opaque:opacity ~idopt:None
   in
-  let pstate = Lemmas.start_proof ~ontop:(Some pstate)
+  let pstate = Lemmas.start_proof
     na
     (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
     sigma gls_type ~hook:(Lemmas.mk_hook hook) in
@@ -1399,7 +1398,7 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type
   try
     Some (fst @@ by (Proofview.V82.tactic tclIDTAC) pstate) (* raises UserError _ if the proof is complete *)
   with UserError _ ->
-    defined pstate
+    (defined pstate; None)
 
 let com_terminate
     tcc_lemma_name
@@ -1413,7 +1412,7 @@ let com_terminate
     nb_args ctx
     hook =
   let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
-    let pstate = Lemmas.start_proof ~ontop:None thm_name
+    let pstate = Lemmas.start_proof 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 in
     let pstate = fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) pstate in
@@ -1431,7 +1430,8 @@ let com_terminate
   with EmptySubgoals ->
     (* a non recursive function declared with measure ! *)
     tcc_lemma_ref := Not_needed;
-    defined pstate
+    defined pstate;
+    None
 
 let start_equation (f:GlobRef.t) (term_f:GlobRef.t)
   (cont_tactic:Id.t list -> tactic) g =
@@ -1459,7 +1459,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
     let evd = Evd.from_ctx uctx in
     let f_constr = constr_of_monomorphic_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
-    let pstate = Lemmas.start_proof ~ontop:None eq_name (Global, false, Proof Lemma) ~sign evd
+    let pstate = Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign evd
        (EConstr.of_constr equation_lemma_type) in
     let pstate = fst @@ by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
@@ -1489,13 +1489,13 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
 	       }
 	  )
        )) pstate in
-    let _ = Flags.silently (fun () -> Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None) () in
+    let _ = Flags.silently (fun () -> Lemmas.save_pstate_proved ~pstate ~opaque:opacity ~idopt: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 : Proof_global.t option =
+    generate_induction_principle using_lemmas : Proof_global.pstate option =
   let open Term in
   let open Constr in
   let open CVars in
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index a006c2c354..84d7a399e1 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -14,6 +14,4 @@ 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 -> Proof_global.t option
-
-
+            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.pstate option