6 files changed, 15 insertions, 29 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 651895aa08..92fa94d6dc 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1487,7 +1487,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 				    Eauto.eauto_with_bases
 				      (true,5)
 				      [(fun _ sigma -> (sigma, Lazy.force refl_equal))]
-				      [Hints.Hint_db.empty empty_transparent_state false]
+                                      [Hints.Hint_db.empty TransparentState.empty false]
 				  )
 			   )
 			)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d1e7d8a5a8..1cf952576d 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -320,10 +320,16 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
     (* 	  let dur1 = System.time_difference tim1 tim2 in *)
     (* 	  Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
     (* 	end; *)
-    get_proof_clean true, CEphemeron.create hook
-  end
-
 
+      let open Proof_global in
+      let { id; entries; persistence } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in
+      match entries with
+      | [entry] ->
+        discard_current ();
+        (id,(entry,persistence)), CEphemeron.create hook
+      | _ ->
+        CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
+  end
 
 let generate_functional_principle (evd: Evd.evar_map ref)
     interactive_proof
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 155df1c1e0..7e707b423a 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -186,8 +186,8 @@ VERNAC COMMAND EXTEND Function
            Vernac_classifier.classify_vernac
              (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
          with
-         | Vernacexpr.VtSideff ids, _ when hard ->
-             Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
+         | Vernacextend.VtSideff ids, _ when hard ->
+             Vernacextend.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
          | x -> x }
     -> { do_generate_principle false (List.map snd recsl) }
 END
@@ -225,7 +225,7 @@ let warning_error names e =
 
 VERNAC COMMAND EXTEND NewFunctionalScheme
 | ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
-   => { Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater }
+   => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
    ->
     {
       begin
@@ -261,7 +261,7 @@ END
 
 VERNAC COMMAND EXTEND NewFunctionalCase
 | ["Functional" "Case" fun_scheme_arg(fas) ]
-  => { Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater }
+  => { Vernacextend.(VtSideff[pi1 fas], VtLater) }
   -> { Functional_principles_types.build_case_scheme fas }
 END
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index cd2ea3ef88..b68b34ca35 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -147,17 +147,6 @@ let save with_clean id const (locality,_,kind) hook =
   CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
   definition_message id
 
-
-
-let cook_proof _ =
-  let (id,(entry,_,strength)) = Pfedit.cook_proof () in
-  (id,(entry,strength))
-
-let get_proof_clean do_reduce =
-  let result = cook_proof do_reduce in
-  Proof_global.discard_current ();
-  result
-
 let with_full_print f a =
   let old_implicit_args = Impargs.is_implicit_args ()
   and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 0c8f40c5cf..c9d153d89f 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -45,15 +45,6 @@ val jmeq_refl : unit -> EConstr.constr
 val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry  -> Decl_kinds.goal_kind ->
   Lemmas.declaration_hook CEphemeron.key -> unit
 
-(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
-   abort the proof
-*)
-val get_proof_clean : bool ->
-  Names.Id.t *
-    (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind)
-
-
-
 (* [with_full_print f a] applies [f] to [a] in full printing environment.
 
    This function preserves the print settings
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 63a3e0582d..6e5e3f9353 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1359,7 +1359,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 		      Eauto.eauto_with_bases
 			(true,5)
 			[(fun _ sigma -> (sigma, (Lazy.force refl_equal)))]
-			[Hints.Hint_db.empty empty_transparent_state false]
+                        [Hints.Hint_db.empty TransparentState.empty false]
 		      ]
 		    )
 		  )