Factoring(continued).

This commit removes the hook.

4 files changed, 10 insertions, 10 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 3d577b440..2661a78a5 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -289,12 +289,13 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
   let new_princ_name =
     next_ident_away_in_goal (Id.of_string "___________princ_________") []
   in
+  let hook = hook new_principle_type in
   begin
     Lemmas.start_proof
       new_princ_name
       (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
       new_principle_type
-      (hook new_principle_type)
+      hook
     ;
     (*       let _tim1 = System.get_time ()  in *)
     ignore (Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams)));
@@ -303,7 +304,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
     (* 	  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
+    get_proof_clean true,Ephemeron.create hook
   end
 
 
@@ -359,7 +360,7 @@ let generate_functional_principle
       register_with_sort InProp;
       register_with_sort InSet
   in
-  let (id,(entry,g_kind,hook)) =
+  let ((id,(entry,g_kind)),hook) =
     build_functional_principle interactive_proof old_princ_type new_sorts funs i
     proof_tac hook
   in
@@ -511,7 +512,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
 	s::l_schemes -> s,l_schemes
       | _ -> anomaly (Pp.str "")
   in
-  let (_,(const,_,_)) =
+  let ((_,(const,_)),_) =
     try
       build_functional_principle false
 	first_type
@@ -585,7 +586,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
 	   (* If we reach this point, the two principle are not mutually recursive
 	      We fall back to the previous method
 	   *)
-	     let (_,(const,_,_)) =
+	     let ((_,(const,_)),_) =
 	       build_functional_principle
 		 false
 		 (List.nth other_princ_types (!i - 1))
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 604d7d853..5c37dcec3 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -166,8 +166,8 @@ let save with_clean id const (locality,kind) hook =
 
 
 let cook_proof _ =
-  let (id,(entry,strength,hook)) = Pfedit.cook_proof (fun _ -> ()) in
-  (id,(entry,strength,hook))
+  let (id,(entry,strength)) = Pfedit.cook_proof () in
+  (id,(entry,strength))
 
 let get_proof_clean do_reduce =
   let result = cook_proof do_reduce in
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index cea5ffe25..0e8b22deb 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -54,8 +54,7 @@ val save : bool -> Id.t ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
 *)
 val get_proof_clean : bool ->
   Names.Id.t *
-    (Entries.definition_entry * Decl_kinds.goal_kind *
-      unit Tacexpr.declaration_hook Ephemeron.key)
+    (Entries.definition_entry * Decl_kinds.goal_kind)
 
 
 
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 83a4d425b..5f26e2bac 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -412,7 +412,7 @@ let show_pftreestate internal fn (kind,pftst) id =
 
 let show fn =
  let pftst = Pfedit.get_pftreestate () in
- let (id,kind,_,_) = Pfedit.current_proof_statement () in
+ let (id,kind,_) = Pfedit.current_proof_statement () in
   show_pftreestate false fn (kind,pftst) id
 ;;