Merge PR #10215: Refine typing of vernacular commands

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares

19 files changed, 312 insertions, 260 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 4769c2dc53..9c1882dc9a 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -101,8 +101,8 @@ let start_deriving f suchthat lemma =
       in
 
   let terminator = Proof_global.make_terminator terminator in
-  let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in
-  Proof_global.simple_with_current_proof begin fun _ p ->
+  let pstate = Proof_global.start_dependent_proof lemma kind goals terminator in
+  Proof_global.modify_proof begin fun p ->
     let p,_,() =  Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in
     p
   end pstate
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index 214a9d8bb5..526989fdf3 100644
--- a/plugins/derive/g_derive.mlg
+++ b/plugins/derive/g_derive.mlg
@@ -22,7 +22,7 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac
 
 }
 
-VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command }
-| ![ proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
-  { fun ~pstate -> Some Derive.(start_deriving f suchthat lemma) }
+VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof
+| [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
+  { Derive.(start_deriving f suchthat lemma) }
 END
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 8f17f7b2dd..c5439ffaf6 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -751,10 +751,6 @@ let extract_and_compile l =
 
 (* Show the extraction of the current ongoing proof *)
 let show_extraction ~pstate =
-  let pstate = match pstate with
-    | None -> CErrors.user_err Pp.(str "No ongoing proof")
-    | Some pstate -> pstate
-  in
   init ~inner:true false false;
   let prf = Proof_global.give_me_the_proof pstate in
   let sigma, env = Pfedit.get_current_context pstate in
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 7ba7e05019..7d04fee7c1 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -40,4 +40,4 @@ val structure_for_compute :
 
 (* Show the extraction of the current ongoing proof *)
 
-val show_extraction : pstate:Proof_global.t option -> unit
+val show_extraction : pstate:Proof_global.t -> unit
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index db1a389fe7..9ea3fbeaf4 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -177,7 +177,7 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF
 END
 (* Show the extraction of the current proof *)
 
-VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY
-| ![ proof ] [ "Show" "Extraction" ]
-  -> { fun ~pstate -> let () = show_extraction ~pstate in pstate }
+VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY STATE proof_query
+| [ "Show" "Extraction" ]
+  -> { show_extraction }
 END
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..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
-| ![ 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
-           | _,((_,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) }
+VERNAC COMMAND EXTEND Function STATE CUSTOM
+| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
+    => { 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
 
 {
@@ -225,33 +242,32 @@ let warning_error names e =
 }
 
 VERNAC COMMAND EXTEND NewFunctionalScheme
-| ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
+| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
    => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
    ->
-    { fun ~pstate ->
-      begin
+    { begin
         try
-          Functional_principles_types.build_scheme fas; pstate
+          Functional_principles_types.build_scheme fas
         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
+                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; pstate
+          warning_error names e
       end
     }
 END
@@ -265,6 +281,6 @@ END
 
 (***** debug only ***)
 VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
-| ![ proof ] ["Generate" "graph" "for" reference(c)] ->
+| ["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 a6b088de0c..241da053b7 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
+       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 ~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 generate_correction_proof_wf f_ref tcc_lemma_ref
@@ -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 ~pstate 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,8 +660,8 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive
 	      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
-          else pstate, 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 =
 	    match recompute_binder_list [fixpoint_expr] with 
@@ -684,8 +684,8 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive
 	      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
-          else pstate, 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) ->
 		       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,9 @@ 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 (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 ->
@@ -902,11 +902,27 @@ 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_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;
-         pstate)
-
-let do_generate_principle = do_generate_principle [] warning_error true
+           expr_list)
+
+(* *************** 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 acf85f539e..1ba245a45d 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -5,10 +5,12 @@ 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 ->
-  bool ->
+val do_generate_principle :
+  (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 ->
@@ -17,4 +19,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 : GlobRef.t -> unit
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..e2321d233c 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
@@ -1396,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
+  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
@@ -1413,7 +1410,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 +1428,8 @@ let com_terminate
   with EmptySubgoals ->
     (* a non recursive function declared with measure ! *)
     tcc_lemma_ref := Not_needed;
-    defined pstate
+    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 =
@@ -1459,7 +1457,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,12 +1487,12 @@ 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
+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 a006c2c354..b92ac3a0ec 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -5,15 +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
-
 
+val recursive_definition :  
+  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
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4c186dce09..0ded60d9c7 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -931,10 +931,10 @@ END
 (* spiwack: I put it in extratactics because it is somewhat tied with
    the semantics of the LCF-style tactics, hence with the classic tactic
    mode. *)
-VERNAC COMMAND EXTEND GrabEvars
-| ![ proof ] [ "Grab" "Existential" "Variables" ]
+VERNAC COMMAND EXTEND GrabEvars STATE proof
+| [ "Grab" "Existential" "Variables" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p  -> Proof.V82.grab_evars p)) pstate }
+  -> { fun ~pstate -> Proof_global.modify_proof (fun p  -> Proof.V82.grab_evars p) pstate }
 END
 
 (* Shelves all the goals under focus. *)
@@ -963,10 +963,10 @@ TACTIC EXTEND unshelve
 END
 
 (* Command to add every unshelved variables to the focus *)
-VERNAC COMMAND EXTEND Unshelve
-| ![ proof ] [ "Unshelve" ]
+VERNAC COMMAND EXTEND Unshelve STATE proof
+| [ "Unshelve" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p  -> Proof.unshelve p)) pstate  }
+  -> { fun ~pstate -> Proof_global.modify_proof (fun p  -> Proof.unshelve p) pstate  }
 END
 
 (* Gives up on the goals under focus: the goals are considered solved,
@@ -1118,7 +1118,7 @@ END
 
 VERNAC COMMAND EXTEND OptimizeProof
 | ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
-  { fun ~pstate -> Option.map Proof_global.compact_the_proof pstate }
+  { fun ~pstate -> Proof_global.compact_the_proof pstate }
 | [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
   { Gc.compact () }
 END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 7eb34158e8..960e5b76f8 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -376,7 +376,7 @@ let () = declare_int_option {
 
 let vernac_solve ~pstate n info tcom b =
   let open Goal_select in
-  let pstate, status = Proof_global.with_current_proof (fun etac p ->
+  let pstate, status = Proof_global.with_proof (fun etac p ->
       let with_end_tac = if b then Some etac else None in
       let global = match n with SelectAll | SelectList _ -> true | _ -> false in
       let info = Option.append info !print_info_trace in
@@ -388,7 +388,7 @@ let vernac_solve ~pstate n info tcom b =
       let p = Proof.maximal_unfocus Vernacentries.command_focus p in
       p,status) pstate in
   if not status then Feedback.feedback Feedback.AddedAxiom;
-  Some pstate
+  pstate
 
 let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
 
@@ -434,13 +434,13 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false
 
 }
 
-VERNAC { tactic_mode } EXTEND VernacSolve
-| ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
+| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
     { classify_as_proofstep } -> {
     let g = Option.default (Goal_select.get_default_goal_selector ()) g in
-    Vernacentries.vernac_require_open_proof vernac_solve g n t def
+    vernac_solve g n t def
   }
-| ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
     {
       let anon_abstracting_tac = is_anonymous_abstract t in
       let solving_tac = is_explicit_terminator t in
@@ -450,7 +450,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve
       VtLater
     } -> {
       let t = rm_abstract t in
-      Vernacentries.vernac_require_open_proof vernac_solve Goal_select.SelectAll n t def
+      vernac_solve Goal_select.SelectAll n t def
     }
 END
 
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index de3a9c9fa9..58c8dabd79 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -80,25 +80,25 @@ GRAMMAR EXTEND Gram
 
 open Obligations
 
-let obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.obligation ~ontop:pstate obl t) tac)
-let next_obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.next_obligation ~ontop:pstate obl t) tac)
+let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
+let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
 
 let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
 
 }
 
-VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl }
-| ![ proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_proof
+| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, Some name, Some t) tac }
-| ![ proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
     { obligation (num, Some name, None) tac }
-| ![ proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, None, Some t) tac }
-| ![ proof ] [ "Obligation" integer(num) withtac(tac) ] ->
+| [ "Obligation" integer(num) withtac(tac) ] ->
     { obligation (num, None, None) tac }
-| ![ proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
+| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
     { next_obligation (Some name) tac }
-| ![ proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
+| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
 END
 
 VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 2fad1f6b6a..1a84158df7 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -180,34 +180,34 @@ TACTIC EXTEND setoid_rewrite
 END
 
 VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
         "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) (Some lemma2) None }
 
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
         "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) None None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
       { declare_relation atts a aeq n None None None }
 END
 
 VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
       { declare_relation atts a aeq n None (Some lemma2) None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
       { declare_relation atts a aeq n None (Some lemma2) (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) None (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
         "as" ident(n) ] ->
       { declare_relation atts a aeq n None None (Some lemma3) }
 END
@@ -234,65 +234,63 @@ GRAMMAR EXTEND Gram
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)
         "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)
         "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) None None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None None None }
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None (Some lemma2) None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
         "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None None (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      {
          add_setoid atts [] a aeq t n
      }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      {
          add_setoid atts binders a aeq t n
      }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
-    (* This command may or may not open a goal *)
-    => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater }
-    -> {
-          add_morphism_infer atts m n
-       }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
+  | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
+    => { VtStartProof(GuaranteesOpacity, [n]), VtLater }
+    -> { if Lib.is_modtype () then
+           CErrors.user_err Pp.(str "Add Morphism cannot be used in a module type. Use Parameter Morphism instead.");
+         add_morphism_interactive atts m n }
+  | #[ atts = rewrite_attributes; ] [ "Declare" "Morphism" constr(m) ":" ident(n) ]
+    => { VtSideff([n]), VtLater }
+    -> { add_morphism_as_parameter atts m n }
+  | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
     => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
-    -> {
-          add_morphism atts [] m s n
-       }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
+    -> { add_morphism atts [] m s n }
+  | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
     => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
-    -> {
-          add_morphism atts binders m s n
-       }
+    -> { add_morphism atts binders m s n }
 END
 
 TACTIC EXTEND setoid_symmetry
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 164bd7e118..7b286e69dc 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -23,7 +23,6 @@ open Tacticals.New
 open Tactics
 open Pretype_errors
 open Typeclasses
-open Classes
 open Constrexpr
 open Globnames
 open Evd
@@ -43,13 +42,13 @@ module NamedDecl = Context.Named.Declaration
 
 (** Typeclass-based generalized rewriting. *)
 
-type rewrite_attributes = { polymorphic : bool; program : bool; global : bool }
+type rewrite_attributes = { polymorphic : bool; global : bool }
 
 let rewrite_attributes =
   let open Attributes.Notations in
   Attributes.(polymorphic ++ program ++ locality) >>= fun ((polymorphic, program), locality) ->
   let global = not (Locality.make_section_locality locality) in
-  Attributes.Notations.return { polymorphic; program; global }
+  Attributes.Notations.return { polymorphic; global }
 
 (** Constants used by the tactic. *)
 
@@ -1795,15 +1794,16 @@ let declare_an_instance n s args =
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
-let anew_instance ~pstate atts binders (name,t) fields =
-  let program_mode = atts.program in
-  new_instance ~pstate ~program_mode atts.polymorphic
-    name binders t (Some (true, CAst.make @@ CRecord (fields)))
-    ~global:atts.global ~generalize:false Hints.empty_hint_info
+let anew_instance atts binders (name,t) fields =
+  let _id = Classes.new_instance atts.polymorphic
+      name binders t (true, CAst.make @@ CRecord (fields))
+      ~global:atts.global ~generalize:false Hints.empty_hint_info
+  in
+  ()
 
-let declare_instance_refl ~pstate atts binders a aeq n lemma =
+let declare_instance_refl atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
-  in anew_instance ~pstate atts binders instance
+  in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "reflexivity"),lemma)]
 
 let declare_instance_sym atts binders a aeq n lemma =
@@ -1816,44 +1816,44 @@ let declare_instance_trans atts binders a aeq n lemma =
   in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "transitivity"),lemma)]
 
-let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans =
+let declare_relation atts ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
   let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in
-  let _, pstate = anew_instance ~pstate atts binders instance [] in
+  let () = anew_instance atts binders instance [] in
   match (refl,symm,trans) with
-      (None, None, None) -> pstate
-    | (Some lemma1, None, None) ->
-      snd @@ declare_instance_refl ~pstate atts binders a aeq n lemma1
-    | (None, Some lemma2, None) ->
-      snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2
-    | (None, None, Some lemma3) ->
-      snd @@ declare_instance_trans ~pstate atts binders a aeq n lemma3
-    | (Some lemma1, Some lemma2, None) ->
-      let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
-      snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2
-    | (Some lemma1, None, Some lemma3) ->
-        let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
-        let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
-        let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in
-        snd @@ anew_instance ~pstate atts binders instance
-              [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
-               (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]
-    | (None, Some lemma2, Some lemma3) ->
-        let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
-        let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
-        let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in
-        snd @@ anew_instance ~pstate atts binders instance
-              [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
-               (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]
-     | (Some lemma1, Some lemma2, Some lemma3) ->
-        let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
-        let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
-        let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
-        let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in
-        snd @@ anew_instance ~pstate atts binders instance
-            [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
-             (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
-             (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]
+    (None, None, None) -> ()
+  | (Some lemma1, None, None) ->
+    declare_instance_refl atts binders a aeq n lemma1
+  | (None, Some lemma2, None) ->
+    declare_instance_sym atts binders a aeq n lemma2
+  | (None, None, Some lemma3) ->
+    declare_instance_trans atts binders a aeq n lemma3
+  | (Some lemma1, Some lemma2, None) ->
+    let () = declare_instance_refl atts binders a aeq n lemma1 in
+    declare_instance_sym atts binders a aeq n lemma2
+  | (Some lemma1, None, Some lemma3) ->
+    let () = declare_instance_refl atts binders a aeq n lemma1 in
+    let () = declare_instance_trans atts binders a aeq n lemma3 in
+    let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in
+    anew_instance atts binders instance
+      [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
+       (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]
+  | (None, Some lemma2, Some lemma3) ->
+    let () = declare_instance_sym atts binders a aeq n lemma2 in
+    let () = declare_instance_trans atts binders a aeq n lemma3 in
+    let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in
+    anew_instance atts binders instance
+      [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
+       (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]
+  | (Some lemma1, Some lemma2, Some lemma3) ->
+    let () = declare_instance_refl atts binders a aeq n lemma1 in
+    let () = declare_instance_sym atts binders a aeq n lemma2 in
+    let () = declare_instance_trans atts binders a aeq n lemma3 in
+    let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in
+    anew_instance atts binders instance
+      [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
+       (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
+       (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]
 
 let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
 
@@ -1949,18 +1949,18 @@ let warn_add_setoid_deprecated =
   CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
       Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation."))
 
-let add_setoid ~pstate atts binders a aeq t n =
+let add_setoid atts binders a aeq t n =
   warn_add_setoid_deprecated ?loc:a.CAst.loc ();
   init_setoid ();
-  let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
-  let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
-  let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
+  let () = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
+  let () = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+  let () = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in
-  snd @@ anew_instance ~pstate atts binders instance
-      [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
-       (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
-       (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]
+  anew_instance atts binders instance
+    [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
+     (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
+     (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]
 
 
 let make_tactic name =
@@ -1972,45 +1972,48 @@ let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
       Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
 
-let add_morphism_infer ~pstate atts m n : Proof_global.t option =
+let add_morphism_as_parameter atts m n : unit =
+  init_setoid ();
+  let instance_id = add_suffix n "_Proper" in
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let uctx, instance = build_morphism_signature env evd m in
+  let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
+  let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
+      (Entries.ParameterEntry
+         (None,(instance,uctx),None),
+       Decl_kinds.IsAssumption Decl_kinds.Logical)
+  in
+  Classes.add_instance (Classes.mk_instance
+                  (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
+  declare_projection n instance_id (ConstRef cst)
+
+let add_morphism_interactive atts m n : Proof_global.t =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   init_setoid ();
-  (* NB: atts.program is ignored, program mode automatically set by vernacentries *)
   let instance_id = add_suffix n "_Proper" in
   let env = Global.env () in
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
-    if Lib.is_modtype () then
-      let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
-      let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
-          (Entries.ParameterEntry
-             (None,(instance,uctx),None),
-           Decl_kinds.IsAssumption Decl_kinds.Logical)
-      in
-      add_instance (Classes.mk_instance
-                      (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
-      declare_projection n instance_id (ConstRef cst);
-      pstate
-    else
-      let kind = Decl_kinds.Global, atts.polymorphic,
-                 Decl_kinds.DefinitionBody Decl_kinds.Instance
-      in
-      let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
-      let hook _ _ _ = function
-        | Globnames.ConstRef cst ->
-          add_instance (Classes.mk_instance
-                          (PropGlobal.proper_class env evd) Hints.empty_hint_info
-                          atts.global (ConstRef cst));
-          declare_projection n instance_id (ConstRef cst)
-        | _ -> assert false
-      in
-      let hook = Lemmas.mk_hook hook in
-      Flags.silently
-        (fun () ->
-           let pstate = Lemmas.start_proof ~ontop:pstate ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
-           Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) ()
+  let kind = Decl_kinds.Global, atts.polymorphic,
+             Decl_kinds.DefinitionBody Decl_kinds.Instance
+  in
+  let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
+  let hook _ _ _ = function
+    | Globnames.ConstRef cst ->
+      Classes.add_instance (Classes.mk_instance
+                      (PropGlobal.proper_class env evd) Hints.empty_hint_info
+                      atts.global (ConstRef cst));
+      declare_projection n instance_id (ConstRef cst)
+    | _ -> assert false
+  in
+  let hook = Lemmas.mk_hook hook in
+  Flags.silently
+    (fun () ->
+       let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+       fst Pfedit.(by (Tacinterp.interp tac) pstate)) ()
 
-let add_morphism ~pstate atts binders m s n =
+let add_morphism atts binders m s n =
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
   let instance_name = (CAst.make @@ Name instance_id),None in
@@ -2020,12 +2023,12 @@ let add_morphism ~pstate atts binders m s n =
        [cHole; s; m])
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
-  let _, pstate = new_instance ~pstate
-      ~program_mode:atts.program ~global:atts.global atts.polymorphic
-      instance_name binders instance_t None
+  let _id, pstate = Classes.new_instance_interactive
+      ~global:atts.global atts.polymorphic
+      instance_name binders instance_t
       ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
   in
-  pstate
+  pstate (* no instance body -> always open proof *)
 
 (** Bind to "rewrite" too *)
 
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index a200cb5ced..3ef33c6dc9 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -81,18 +81,36 @@ val cl_rewrite_clause :
 val is_applied_rewrite_relation :
   env -> evar_map -> rel_context -> constr -> types option
 
-val declare_relation : pstate:Proof_global.t option -> rewrite_attributes ->
-  ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
-  constr_expr option -> constr_expr option -> constr_expr option -> Proof_global.t option
-
-val add_setoid : pstate:Proof_global.t option ->
-  rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
-  Id.t -> Proof_global.t option
-
-val add_morphism_infer : pstate:Proof_global.t option -> rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option
-
-val add_morphism : pstate:Proof_global.t option ->
-  rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option
+val declare_relation
+  : rewrite_attributes
+  -> ?binders:local_binder_expr list
+  -> constr_expr
+  -> constr_expr
+  -> Id.t
+  -> constr_expr option
+  -> constr_expr option
+  -> constr_expr option
+  -> unit
+
+val add_setoid
+  : rewrite_attributes
+  -> local_binder_expr list
+  -> constr_expr
+  -> constr_expr
+  -> constr_expr
+  -> Id.t
+  -> unit
+
+val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t
+val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit
+
+val add_morphism
+  : rewrite_attributes
+  -> local_binder_expr list
+  -> constr_expr
+  -> constr_expr
+  -> Id.t
+  -> Proof_global.t
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr