Modules dans COQ\!\!\!\!

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

7 files changed, 15 insertions, 10 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e2932a904..8b47ced02 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -15,6 +15,7 @@ open Nameops
 open Sign
 open Term
 open Declarations
+open Entries
 open Environ
 open Evd
 open Declare
@@ -34,7 +35,7 @@ open Safe_typing
 type proof_topstate = {
   top_hyps : named_context * named_context;
   top_goal : goal;
-  top_strength : bool * Nametab.strength;
+  top_strength : bool * Libnames.strength;
   top_hook : declaration_hook }
 
 let proof_edits =
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 78314eacb..beeb56959 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -67,7 +67,7 @@ val get_undo : unit -> int option
     declare the built constructions as a coercion or a setoid morphism) *)
 
 val start_proof : 
-  identifier -> bool * strength -> named_context -> constr
+  identifier -> bool * Libnames.strength -> named_context -> constr
     -> declaration_hook -> unit
 
 (* [restart_proof ()] restarts the current focused proof from the beginning
@@ -96,7 +96,7 @@ val suspend_proof : unit -> unit
 
 val cook_proof : unit -> 
   identifier *
-  (Safe_typing.constant_entry * (bool * strength) * declaration_hook)
+  (Entries.definition_entry * (bool * Libnames.strength) * declaration_hook)
 
 (* To export completed proofs to xml *)
 val set_xml_cook_proof : (pftreestate -> unit) -> unit
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 0c916495a..a05464b00 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -21,6 +21,7 @@ open Evarutil
 open Proof_type
 open Tacred
 open Typing
+open Libnames
 open Nametab
 
 (*
@@ -277,9 +278,9 @@ let last_of_cvt_flags red =
      List.map
        (function
 	  | EvalVarRef id -> nvar id
-	  | EvalConstRef sp ->
+	  | EvalConstRef kn ->
 	      ast_of_qualid
-                (shortest_qualid_of_global (Global.env()) (ConstRef sp)))
+                (shortest_qualid_of_global None (ConstRef kn)))
        lconst in
    if lqid = [] then []
    else if n_unf then [ope("Delta",[]);ope("UnfBut",lqid)]
@@ -303,9 +304,9 @@ let ast_of_cvt_redexp = function
     ope("Unfold",List.map (fun (locc,sp) -> ope("UNFOLD",
       [match sp with
 	| EvalVarRef id -> nvar id
-	| EvalConstRef sp -> 					
+	| EvalConstRef kn -> 					
 	    ast_of_qualid
-	      (shortest_qualid_of_global (Global.env()) (ConstRef sp))]
+	      (shortest_qualid_of_global None (ConstRef kn))]
       @(List.map num locc))) l)
   | Fold l ->
     ope("Fold",List.map (fun c -> ope ("CONSTR",
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 756370b80..3d599cc48 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -12,6 +12,7 @@
 open Environ
 open Evd
 open Names
+open Libnames
 open Term
 open Util
 open Tacexpr
@@ -99,4 +100,4 @@ type closed_generic_argument =
 type 'a closed_abstract_argument_type =
     ('a,constr,raw_tactic_expr) abstract_argument_type
 
-type declaration_hook = Nametab.strength -> Nametab.global_reference -> unit
+type declaration_hook = Libnames.strength -> global_reference -> unit
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 9c4bf5c47..6f86fbe3a 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -12,6 +12,7 @@
 open Environ
 open Evd
 open Names
+open Libnames
 open Term
 open Util
 open Tacexpr
@@ -127,4 +128,4 @@ type closed_generic_argument =
 type 'a closed_abstract_argument_type =
     ('a,constr,raw_tactic_expr) abstract_argument_type
 
-type declaration_hook = Nametab.strength -> Nametab.global_reference -> unit
+type declaration_hook = Libnames.strength -> global_reference -> unit
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 65c9cd009..2e8d581ae 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -10,6 +10,7 @@
 
 open Names
 open Coqast
+open Libnames
 open Nametab
 open Rawterm
 open Util
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 7777f3463..e0b802c3e 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -83,7 +83,7 @@ let pf_interp_type gls c =
   let evc = project gls in 
   Astterm.interp_type evc (pf_env gls) c
 
-let pf_global gls id = Declare.construct_reference (pf_env gls) id
+let pf_global gls id = Declare.construct_reference (Some (pf_hyps gls)) id
 
 let pf_parse_const gls = compose (pf_global gls) id_of_string