5 files changed, 10 insertions, 56 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index e2cad94495..bef89909de 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -35,7 +35,7 @@ let observennl strm =
 let do_observe_tac s tac g =
  try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
  with e ->
-   let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
+   let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
    msgnl (str "observation "++ s++str " raised exception " ++
 	    Cerrors.explain_exn e ++ str " on goal " ++ goal );
    raise e;;
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 0f048f59a0..ff7089613f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -180,48 +180,9 @@ let save with_clean id const (locality,kind) hook =
 
 
 
-
-let extract_pftreestate pts =
-  let pfterm,subgoals = Refiner.extract_open_pftreestate pts in
-  let tpfsigma = Refiner.evc_of_pftreestate pts in
-  let exl = Evarutil.non_instantiated tpfsigma  in
-  if subgoals <> [] or exl <> [] then
-    Util.errorlabstrm "extract_proof"
-      (if subgoals <> [] then
-        str "Attempt to save an incomplete proof"
-      else
-        str "Attempt to save a proof with existential variables still non-instantiated");
-  let env = Global.env_of_context (Refiner.proof_of_pftreestate pts).Proof_type.goal.Evd.evar_hyps in
-  env,tpfsigma,pfterm
-
-
-let nf_betaiotazeta =
-  let clos_norm_flags flgs env sigma t =
-    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
-  clos_norm_flags Closure.betaiotazeta
-
-let nf_betaiota =
-  let clos_norm_flags flgs env sigma t =
-    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
-  clos_norm_flags Closure.betaiota
-
-let cook_proof do_reduce =
-  let pfs = Pfedit.get_pftreestate ()
-(*   and ident = Pfedit.get_current_proof_name ()  *)
-  and (ident,strength,concl,hook) = Pfedit.current_proof_statement ()  in
-  let env,sigma,pfterm = extract_pftreestate pfs in
-  let pfterm =
-    if do_reduce
-    then nf_betaiota env sigma pfterm
-    else pfterm
-  in
-  (ident,
-   ({ const_entry_body = pfterm;
-      const_entry_type = Some concl;
-      const_entry_opaque = false;
-      const_entry_boxed = false},
-    strength, hook))
-
+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
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 6f6607fccc..c48dff0c63 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -50,15 +50,8 @@ 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]
-
-
-
-   DON'T USE IT if you cannot ensure that there is no VMcast in the proof
-
 *)
 
-(* val nf_betaiotazeta : Reductionops.reduction_function *)
-
 val new_save_named : bool -> unit
 
 val save : bool -> identifier ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 8c22265d66..28de815ca0 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -60,7 +60,7 @@ let observennl strm =
 
 
 let do_observe_tac s tac g =
-  let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
+  let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
   try
     let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
   with e ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1eae097189..8dc660b421 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -85,7 +85,7 @@ let rec print_debug_queue e =
   
 
 let do_observe_tac s tac g = 
-  let goal = Printer.pr_goal (sig_it g) in
+  let goal = Printer.pr_goal g in
   let lmsg = (str "recdef ") ++ (str s) in 
   Queue.add (lmsg,goal) debug_queue;
   try 
@@ -376,7 +376,7 @@ let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
 		(fun g1 ->
 		   let ty_teq = pf_type_of g1 (mkVar teq) in
 		   let teq_lhs,teq_rhs =
-		     let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal (sig_it g1) ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in
+		     let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal g1 ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in
 		     args.(1),args.(2)
 		   in
 	           cont_function (mkVar teq::eqs) (replace_term teq_lhs teq_rhs expr) g1
@@ -884,9 +884,9 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
   end
 
 let get_current_subgoals_types () =
-  let pts =  get_pftreestate () in
-  let _,subs = extract_open_pftreestate pts in
-  List.map snd ((* List.sort (fun (x,_) (y,_) -> x -y ) *)subs )
+  let p = Proof_global.give_me_the_proof () in
+  let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in
+  List.map (Goal.V82.abstract_type sigma) sgs
 
 let build_and_l l =
   let and_constr =  Coqlib.build_coq_and () in