5 files changed, 10 insertions, 23 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 52ba41869a..f4e8589031 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -983,7 +983,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
     lemma_type
     (fun _ _ -> ());
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
-  Lemmas.save_named false
+  Lemmas.save_proof (Vernacexpr.Proved(false,None))
 
 
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b7072ea3bd..db4297b37d 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -169,11 +169,6 @@ let cook_proof _ =
   let (id,(entry,_,strength,hook)) = Pfedit.cook_proof (fun _ -> ()) in
   (id,(entry,strength,hook))
 
-let new_save_named opacity =
-  let id,(const,persistence,hook) = cook_proof true  in
-  let const = { const with const_entry_opaque = opacity } in
-  save true id const persistence hook
-
 let get_proof_clean do_reduce =
   let result = cook_proof do_reduce in
   Pfedit.delete_current_proof ();
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 722f857b34..cea5ffe259 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -46,12 +46,6 @@ val const_of_id: Id.t -> constant
 val jmeq : unit -> Term.constr
 val jmeq_refl : unit -> Term.constr
 
-(* [save_named] is a copy of [Command.save_named] but uses
-   [nf_betaiotazeta] instead of [nf_betaiotaevar_preserving_vm_cast]
-*)
-
-val new_save_named : bool -> unit
-
 val save : bool -> Id.t ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
   unit Tacexpr.declaration_hook Ephemeron.key -> unit
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 0d32bf2bc9..7c8f5714e6 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1008,7 +1008,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 
 
 
-let do_save () = Lemmas.save_named false
+let do_save () = Lemmas.save_proof (Vernacexpr.Proved(false,None))
 
 
 (* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6afbff779d..082d7ad51e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -64,7 +64,7 @@ let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) =
           const_entry_inline_code = false} in
       ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
 
-let defined () = Lemmas.save_named false
+let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None))
 
 let def_of_const t =
    match (kind_of_term t) with
@@ -1249,7 +1249,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	with e when Errors.noncritical e ->
           anomaly (Pp.str "open_new_goal with an unamed theorem")
   in
-  let sign = initialize_named_context_for_proof () in
   let na = next_global_ident_away name [] in
   if Termops.occur_existential gls_type then
     Errors.error "\"abstract\" cannot handle existentials";
@@ -1309,12 +1308,11 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	       )
       		 g)
 ;
-    Lemmas.save_named opacity;
+    Lemmas.save_proof (Vernacexpr.Proved(opacity,None));
   in
-  start_proof
+  Lemmas.start_proof
     na
     (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma)
-    sign
     gls_type
     hook;
   if Indfun_common.is_strict_tcc  ()
@@ -1360,8 +1358,8 @@ let com_terminate
     hook =
   let start_proof (tac_start:tactic) (tac_end:tactic) =
     let (evmap, env) = Lemmas.get_current_context() in
-    start_proof thm_name
-      (Global, Proof Lemma) (Environ.named_context_val env)
+    Lemmas.start_proof thm_name
+      (Global, Proof Lemma) ~sign:(Environ.named_context_val env)
       (compute_terminate_type nb_args fonctional_ref) hook;
 
     ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)));
@@ -1408,8 +1406,8 @@ let (com_eqn : int -> Id.t ->
     let (evmap, env) = Lemmas.get_current_context() in
     let f_constr = constr_of_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
-    (start_proof eq_name (Global, Proof Lemma)
-       (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
+    (Lemmas.start_proof eq_name (Global, Proof Lemma)
+       ~sign:(Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
      ignore (by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
 	  (fun  x ->
@@ -1440,7 +1438,7 @@ let (com_eqn : int -> Id.t ->
        ))); 
      (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
 (*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
-     Flags.silently (fun () -> Lemmas.save_named opacity) () ; 
+     Flags.silently (fun () -> Lemmas.save_proof (Vernacexpr.Proved(opacity,None))) () ; 
 (*      Pp.msgnl (str "eqn finished"); *)
     );;