From 8abacf00c6c39ec98085d531737d18edc9c19b2a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 2 May 2019 19:46:02 +0200
Subject: 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.
---
 plugins/funind/functional_principles_proofs.ml |  9 ++++----
 plugins/funind/functional_principles_types.ml  | 11 +++++----
 plugins/funind/g_indfun.mlg                    | 18 ++++++++-------
 plugins/funind/indfun.ml                       | 31 +++++++++++++++-----------
 plugins/funind/indfun.mli                      |  6 ++---
 plugins/funind/invfun.ml                       |  8 +++----
 plugins/funind/recdef.ml                       | 20 ++++++++---------
 plugins/funind/recdef.mli                      |  4 +---
 8 files changed, 56 insertions(+), 51 deletions(-)

(limited to 'plugins/funind')

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
-- 
cgit v1.2.3


From b8842c3c8d6e6d9d4c19a75453fca9f94de6fa49 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 3 May 2019 14:14:40 +0200
Subject: coqpp: add new ![] specifiers for structured proof interaction

![proof_stack] is equivalent to the old meaning of ![proof]: the body
has type `pstate:Proof_global.t option -> Proof_global.t option`

The other specifiers are for the following body types:

~~~
![open_proof] `is_ontop:bool -> pstate`

![maybe_open_proof] `is_ontop:bool -> pstate option`

![proof] `pstate:pstate -> pstate`

![proof_opt_query] `pstate:pstate option -> unit`

![proof_query] `pstate:pstate -> unit`
~~~

The `is_ontop` is only used for the warning message when declaring a
section variable inside a proof, we could also just stop warning.

The specifiers look closely related to stm classifiers, but currently
they're unconnected. Notably this means that a ![proof_query] doesn't
have to be classified QUERY.

![proof_stack] is only used by g_rewrite/rewrite whose behaviour I
 don't fully understand, maybe we can drop it in the future.

For compat we may want to consider keeping ![proof] with its old
meaning and using some new name for the new meaning. OTOH fixing
plugins to be stricter is easier if we change it as the errors tell us
where it's used.
---
 plugins/funind/g_indfun.mlg | 25 +++++++++++--------------
 plugins/funind/indfun.ml    | 11 +++--------
 plugins/funind/indfun.mli   |  2 +-
 3 files changed, 15 insertions(+), 23 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index b8db3dc5ce..cc772e96f3 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
-| ![ proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
+| ![ maybe_open_proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
     => { let hard = List.exists (function
            | _,((_,(Some { CAst.v = CMeasureRec _ }
              | Some { CAst.v = CWfRec _}),_,_,_),_) -> true
@@ -190,9 +190,7 @@ VERNAC COMMAND EXTEND Function
          | Vernacextend.VtSideff ids, _ when hard ->
              Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
          | x -> x }
-    -> { fun ~pstate:ontop ->
-      let pstate = do_generate_principle false (List.map snd recsl) in
-      Proof_global.maybe_push ~ontop pstate}
+    -> { do_generate_principle false (List.map snd recsl) }
 END
 
 {
@@ -227,33 +225,32 @@ let warning_error names e =
 }
 
 VERNAC COMMAND EXTEND NewFunctionalScheme
-| ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
+| ![ maybe_open_proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
    => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
    ->
-    { fun ~pstate:ontop ->
-      begin
+    { begin
         try
-          Functional_principles_types.build_scheme fas; ontop
+          Functional_principles_types.build_scheme fas; None
         with
         | Functional_principles_types.No_graph_found ->
           begin
             match fas with
             | (_,fun_name,_)::_ ->
               begin
-                let ontop = make_graph ~ontop (Smartlocate.global_with_alias fun_name) in
-                try Functional_principles_types.build_scheme fas; ontop
+                let pstate = make_graph (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; ontop
+                  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; ontop
+          warning_error names e; None
       end
     }
 END
@@ -267,6 +264,6 @@ END
 
 (***** debug only ***)
 VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
-| ![ proof ] ["Generate" "graph" "for" reference(c)] ->
-  { fun ~pstate:ontop -> make_graph ~ontop (Smartlocate.global_with_alias c) }
+| ![ maybe_open_proof ] ["Generate" "graph" "for" reference(c)] ->
+  { make_graph (Smartlocate.global_with_alias c) }
 END
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d47c12a7cb..6ea2eb579f 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -839,7 +839,9 @@ let rec get_args b t : Constrexpr.local_binder_expr list *
     | _ -> [],b,t
 
 
-let make_graph env sigma (f_ref : GlobRef.t) =
+let make_graph (f_ref : GlobRef.t) =
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
   let c,c_body =
     match f_ref with
     | ConstRef c ->
@@ -907,11 +909,4 @@ let make_graph env sigma (f_ref : GlobRef.t) =
            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 cf4ef23d1a..c803484617 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -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 : ontop:Proof_global.t option -> GlobRef.t -> Proof_global.t option
+val make_graph : GlobRef.t -> Proof_global.pstate option
-- 
cgit v1.2.3


From 02fda88fc065577f3f9604477db2e03eb4d5a9b4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 7 May 2019 14:34:06 +0200
Subject: Alternate syntax for ![]: VERNAC EXTEND Foo STATE proof

eg ![proof] becomes STATE proof

This commits still supports the old ![]
so there is redundancy:
~~~
VERNAC EXTEND Foo STATE proof
| ...

VERNAC EXTEND Foo
| ![proof] ...
~~~
with the ![] form being local to the rule and the STATE form
applying to the whole EXTEND except for the rules with a ![].
---
 plugins/funind/g_indfun.mlg | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index cc772e96f3..8c9b1e7ba4 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -176,8 +176,8 @@ let () =
 }
 
 (* TASSI: n'importe quoi ! *)
-VERNAC COMMAND EXTEND Function
-| ![ maybe_open_proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
+VERNAC COMMAND EXTEND Function STATE maybe_open_proof
+| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
     => { let hard = List.exists (function
            | _,((_,(Some { CAst.v = CMeasureRec _ }
              | Some { CAst.v = CWfRec _}),_,_,_),_) -> true
@@ -224,8 +224,8 @@ let warning_error names e =
 
 }
 
-VERNAC COMMAND EXTEND NewFunctionalScheme
-| ![ maybe_open_proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
+VERNAC COMMAND EXTEND NewFunctionalScheme STATE maybe_open_proof
+| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
    => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
    ->
     { begin
@@ -263,7 +263,7 @@ VERNAC COMMAND EXTEND NewFunctionalCase
 END
 
 (***** debug only ***)
-VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
-| ![ maybe_open_proof ] ["Generate" "graph" "for" reference(c)] ->
+VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY STATE maybe_open_proof
+| ["Generate" "graph" "for" reference(c)] ->
   { make_graph (Smartlocate.global_with_alias c) }
 END
-- 
cgit v1.2.3


From 445dee163b7a2c9d4cc24da739d743d80fcec529 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 20 May 2019 16:49:03 +0200
Subject: Funind: use maybe_open_proof a bit less

---
 plugins/funind/g_indfun.mlg | 14 +++++++-------
 plugins/funind/indfun.ml    |  4 ++--
 plugins/funind/indfun.mli   |  2 +-
 3 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 8c9b1e7ba4..bdd30aae0a 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -224,33 +224,33 @@ let warning_error names e =
 
 }
 
-VERNAC COMMAND EXTEND NewFunctionalScheme STATE maybe_open_proof
+VERNAC COMMAND EXTEND NewFunctionalScheme
 | ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
    => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
    ->
     { begin
         try
-          Functional_principles_types.build_scheme fas; None
+          Functional_principles_types.build_scheme fas
         with
         | Functional_principles_types.No_graph_found ->
           begin
             match fas with
             | (_,fun_name,_)::_ ->
               begin
-                let pstate = make_graph (Smartlocate.global_with_alias fun_name) in
-                try Functional_principles_types.build_scheme fas; pstate
+                make_graph (Smartlocate.global_with_alias fun_name);
+                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; pstate
+                  warning_error names e
               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; None
+          warning_error names e
       end
     }
 END
@@ -263,7 +263,7 @@ VERNAC COMMAND EXTEND NewFunctionalCase
 END
 
 (***** debug only ***)
-VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY STATE maybe_open_proof
+VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
 | ["Generate" "graph" "for" reference(c)] ->
   { make_graph (Smartlocate.global_with_alias c) }
 END
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 6ea2eb579f..16df34e214 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -903,10 +903,10 @@ let make_graph (f_ref : GlobRef.t) =
 	 in
          let mp = Constant.modpath c in
          let pstate = do_generate_principle [c,Univ.Instance.empty] error_error  false false expr_list in
+         assert (Option.is_empty pstate);
 	 (* We register the infos *)
 	 List.iter
            (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id)))
-           expr_list;
-         pstate)
+           expr_list)
 
 let do_generate_principle = do_generate_principle [] warning_error true
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index c803484617..cd39266378 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -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 : GlobRef.t -> Proof_global.pstate option
+val make_graph : GlobRef.t -> unit
-- 
cgit v1.2.3


From 99154fcb97653c606d2e62e0a0521c4afddff44c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 20 May 2019 17:11:00 +0200
Subject: Rename Proof_global.{pstate -> t}

---
 plugins/funind/indfun.ml  | 2 +-
 plugins/funind/indfun.mli | 2 +-
 plugins/funind/recdef.ml  | 2 +-
 plugins/funind/recdef.mli | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 16df34e214..7c6669d0fc 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -634,7 +634,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
   
 
 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 =
+    (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 pstate, _is_struct =
     match fixpoint_exprl with
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index cd39266378..47d37b29a5 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -8,7 +8,7 @@ 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 ->
-  Proof_global.pstate option
+  Proof_global.t option
 
 val functional_induction :
   bool ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b4d0f092d8..5a682e7231 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1495,7 +1495,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
 
 
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
-    generate_induction_principle using_lemmas : Proof_global.pstate option =
+    generate_induction_principle using_lemmas : Proof_global.t 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 84d7a399e1..90f9c449b1 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -14,4 +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.pstate option
+            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option
-- 
cgit v1.2.3


From 0f1814bcbaafbd93d7c7587eef8826a80b65477f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 17:52:19 +0200
Subject: [function] always open a proof when used with `wf` or `measure`

---
 plugins/funind/g_indfun.mlg | 47 ++++++++++++++++++++++++++++++---------------
 plugins/funind/indfun.ml    | 36 ++++++++++++++++++++++++----------
 plugins/funind/indfun.mli   |  6 ++++--
 plugins/funind/recdef.ml    | 13 ++++++-------
 plugins/funind/recdef.mli   | 24 ++++++++++++++---------
 5 files changed, 83 insertions(+), 43 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index bdd30aae0a..833ff9f1ed 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -173,24 +173,41 @@ let () =
   let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
   Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer
 
+let is_proof_termination_interactively_checked recsl =
+  List.exists (function
+  | _,((_,( Some { CAst.v = CMeasureRec _ }
+          | Some { CAst.v = CWfRec _}),_,_,_),_) -> true
+  | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_)
+  | _,((_,None,_,_,_),_) -> false) recsl
+
+let classify_as_Fixpoint recsl =
+ Vernac_classifier.classify_vernac
+    (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
+
+let classify_funind recsl =
+  match classify_as_Fixpoint recsl with
+  | Vernacextend.VtSideff ids, _
+    when is_proof_termination_interactively_checked recsl ->
+      Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
+  | x -> x
+
+let is_interactive recsl =
+  match classify_funind recsl with
+  | Vernacextend.VtStartProof _, _ -> true
+  | _ -> false
+
 }
 
-(* TASSI: n'importe quoi ! *)
-VERNAC COMMAND EXTEND Function STATE maybe_open_proof
+VERNAC COMMAND EXTEND Function STATE CUSTOM
 | ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
-    => { let hard = List.exists (function
-           | _,((_,(Some { CAst.v = CMeasureRec _ }
-             | Some { CAst.v = CWfRec _}),_,_,_),_) -> true
-           | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_)
-           | _,((_,None,_,_,_),_) -> false) recsl in
-         match
-           Vernac_classifier.classify_vernac
-             (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
-         with
-         | Vernacextend.VtSideff ids, _ when hard ->
-             Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
-         | x -> x }
-    -> { do_generate_principle false (List.map snd recsl) }
+    => { classify_funind recsl }
+    -> {
+         if is_interactive recsl then
+           Vernacextend.VtOpenProof (fun () ->
+             do_generate_principle_interactive (List.map snd recsl))
+         else
+           Vernacextend.VtDefault (fun () ->
+             do_generate_principle (List.map snd recsl)) }
 END
 
 {
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 7c6669d0fc..bb6db1f5cf 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -459,7 +459,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
     tcc_lemma_ref is_mes  rec_arg_num rec_arg_type relation
 
 
-let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
+let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
     pre_hook
     =
   let type_of_f = Constrexpr_ops.mkCProdN args ret_type in
@@ -500,8 +500,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
       (* No proof done *)
       ()
   in
-  Recdef.recursive_definition
-    is_mes fname rec_impls
+  Recdef.recursive_definition ~interactive_proof
+    ~is_mes fname rec_impls
     type_of_f
     wf_rel_expr
     rec_arg_num
@@ -510,7 +510,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
     using_lemmas
 
 
-let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas args ret_type body =
+let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas args ret_type body =
   let wf_arg_type,wf_arg =
     match wf_arg with
       | None ->
@@ -570,7 +570,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	  in
 	  wf_rel_with_mes,false
   in			       
-  register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg
+  register_wf interactive_proof ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg
     using_lemmas args ret_type body
 
 let map_option f = function 
@@ -633,7 +633,7 @@ 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
+let do_generate_principle_aux 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 pstate, _is_struct =
@@ -660,7 +660,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	      true
 	  in
 	  if register_built
-          then register_wf name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false
+          then register_wf interactive_proof name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, 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 =
@@ -684,7 +684,7 @@ 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 interactive_proof 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 None, true
       | _ ->
           List.iter (function ((_na,ord,_args,_body,_type),_not) ->
@@ -902,11 +902,27 @@ let make_graph (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 [c,Univ.Instance.empty] error_error  false false expr_list in
+         let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error  false false expr_list in
          assert (Option.is_empty pstate);
 	 (* We register the infos *)
 	 List.iter
            (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id)))
            expr_list)
 
-let do_generate_principle = do_generate_principle [] warning_error true
+(* *************** statically typed entrypoints ************************* *)
+
+let do_generate_principle_interactive fixl : Proof_global.t =
+  match
+    do_generate_principle_aux [] warning_error true true fixl
+  with
+  | Some pstate -> pstate
+  | None ->
+      CErrors.anomaly
+       (Pp.str"indfun: leaving no open proof in interactive mode")
+
+let do_generate_principle fixl : unit =
+  match do_generate_principle_aux [] warning_error true false fixl  with
+  | Some _pstate ->
+      CErrors.anomaly
+        (Pp.str"indfun: leaving a goal open in non-interactive mode")
+  | None -> ()
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 47d37b29a5..1ba245a45d 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -6,9 +6,11 @@ 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_interactive :
   (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
-  Proof_global.t option
+  Proof_global.t
 
 val functional_induction :
   bool ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5a682e7231..e2321d233c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1395,12 +1395,10 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type
 	       ) tclIDTAC)
             g end) pstate
   in
-  try
-    Some (fst @@ by (Proofview.V82.tactic tclIDTAC) pstate) (* raises UserError _ if the proof is complete *)
-  with UserError _ ->
-    (defined pstate; None)
+  if Proof_global.get_open_goals pstate = 0 then (defined pstate; None) else Some pstate
 
 let com_terminate
+    interactive_proof
     tcc_lemma_name
     tcc_lemma_ref
     is_mes
@@ -1430,8 +1428,8 @@ let com_terminate
   with EmptySubgoals ->
     (* a non recursive function declared with measure ! *)
     tcc_lemma_ref := Not_needed;
-    defined pstate;
-    None
+    if interactive_proof then Some pstate
+    else (defined pstate; None)
 
 let start_equation (f:GlobRef.t) (term_f:GlobRef.t)
   (cont_tactic:Id.t list -> tactic) g =
@@ -1494,7 +1492,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
 (*      Pp.msgnl (fun _ _ -> str "eqn finished"); *)
 
 
-let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
+let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type_of_f r rec_arg_num eq
     generate_induction_principle using_lemmas : Proof_global.t option =
   let open Term in
   let open Constr in
@@ -1585,6 +1583,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   (* XXX STATE Why do we need this... why is the toplevel protection not enough *)
   funind_purify (fun () ->
       let pstate = com_terminate
+          interactive_proof
           tcc_lemma_name
           tcc_lemma_constr
           is_mes functional_ref
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 90f9c449b1..b92ac3a0ec 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -5,13 +5,19 @@ val tclUSER_if_not_mes :
   bool -> 
   Names.Id.t list option -> 
   Tacmach.tactic
+
 val recursive_definition :  
-bool ->
-           Names.Id.t ->
-           Constrintern.internalization_env ->
-           Constrexpr.constr_expr ->
-           Constrexpr.constr_expr ->
-           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
+  interactive_proof:bool ->
+  is_mes:bool ->
+  Names.Id.t ->
+  Constrintern.internalization_env ->
+  Constrexpr.constr_expr ->
+  Constrexpr.constr_expr ->
+  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
-- 
cgit v1.2.3


From a7a6fa3219134004f1fc6c757f1c16281724f38f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 24 May 2019 14:57:33 +0200
Subject: [vernac] more precise types for Add Morph, Instance, and Function

---
 plugins/funind/indfun.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index bb6db1f5cf..241da053b7 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -434,7 +434,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        None, evd,List.rev rev_pconstants
     | _ ->
-      let pstate = ComFixpoint.do_fixpoint Global false fixpoint_exprl in
+       ComFixpoint.do_fixpoint Global false fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
@@ -448,7 +448,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
        in
-       pstate,evd,List.rev rev_pconstants
+       None,evd,List.rev rev_pconstants
 
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
-- 
cgit v1.2.3