Integrated obligations/eterm and program well-founded fixpoint building to toplevel/

The code is not called yet from there.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15035 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 8 insertions, 8 deletions

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index e8b0042008..fc2b251845 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -78,7 +78,7 @@ type lemma_possible_guards = Proof_global.lemma_possible_guards
 val start_proof :
   identifier -> goal_kind -> named_context_val -> constr ->
   ?init_tac:tactic -> ?compute_guard:lemma_possible_guards -> 
-  declaration_hook -> unit
+  unit declaration_hook -> unit
 
 (** [restart_proof ()] restarts the current focused proof from the beginning
    or fails if no proof is focused *)
@@ -112,7 +112,7 @@ val suspend_proof : unit -> unit
 val cook_proof : (Proof.proof -> unit) ->
   identifier *
     (Entries.definition_entry * lemma_possible_guards * goal_kind *
-     declaration_hook)
+     unit declaration_hook)
 
 (** To export completed proofs to xml *)
 val set_xml_cook_proof : (goal_kind * Proof.proof -> unit) -> unit
@@ -136,7 +136,7 @@ val get_current_goal_context : unit -> Evd.evar_map * env
 (** [current_proof_statement] *)
 
 val current_proof_statement :
-  unit -> identifier * goal_kind * types * declaration_hook
+  unit -> identifier * goal_kind * types * unit declaration_hook
 
 (** {6 ... } *)
 (** [get_current_proof_name ()] return the name of the current focused
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 63bc4a7080..071858cd33 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -66,7 +66,7 @@ type lemma_possible_guards = int list list
 type proof_info = {
   strength : Decl_kinds.goal_kind ;
   compute_guard :  lemma_possible_guards;
-  hook :Tacexpr.declaration_hook ;
+  hook : unit Tacexpr.declaration_hook ;
   mode : proof_mode
 }
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 8e09ab9c10..53aab2b9db 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -57,7 +57,7 @@ val start_proof : Names.identifier ->
                           Decl_kinds.goal_kind ->
                           (Environ.env * Term.types) list  ->
                           ?compute_guard:lemma_possible_guards -> 
-                          Tacexpr.declaration_hook -> 
+                          unit Tacexpr.declaration_hook -> 
                           unit
 
 val close_proof : unit -> 
@@ -65,7 +65,7 @@ val close_proof : unit ->
                           (Entries.definition_entry list * 
 			    lemma_possible_guards * 
 			    Decl_kinds.goal_kind * 
-			    Tacexpr.declaration_hook)
+			    unit Tacexpr.declaration_hook)
 
 exception NoSuchProof
 
@@ -133,5 +133,5 @@ module Bullet : sig
 end
 
 module V82 : sig
-  val get_current_initial_conclusions : unit -> Names.identifier *(Term.types list * Decl_kinds.goal_kind * Tacexpr.declaration_hook)
+  val get_current_initial_conclusions : unit -> Names.identifier *(Term.types list * Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
 end
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 90dddb7486..7ad6bda60f 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -343,4 +343,4 @@ type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
 
 type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type
 
-type declaration_hook = locality -> global_reference -> unit
+type 'a declaration_hook = locality -> global_reference -> 'a