Prise en compte du repertoire dans le section path; utilisation de dirpath pour les noms de modules

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

4 files changed, 37 insertions, 27 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 9b3aa06940..2574a3b30f 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -212,7 +212,8 @@ let recognize_number t =
  This is the right way to access to Coq constants in tactics ML code *)
 
 let constant dir s =
-  Declare.global_absolute_reference (make_path dir (id_of_string s) CCI)
+  Declare.global_absolute_reference
+    (make_path ("Zarith"::dir) (id_of_string s) CCI)
 
 (* fast_integer *)
 let coq_xH = lazy (constant ["fast_integer"] "xH")
@@ -337,36 +338,39 @@ let coq_imp_simp = lazy (constant ["auxiliary"] "imp_simp")
 let coq_neq = lazy (constant ["auxiliary"] "neq")
 let coq_Zne = lazy (constant ["auxiliary"] "Zne")
 
-(* Compare_dec *)
-let coq_le_gt_dec = lazy (constant ["Compare_dec"] "le_gt_dec")
+let constant dir s =
+  Declare.global_absolute_reference (make_path dir (id_of_string s) CCI)
 
 (* Peano *)
-let coq_le = lazy (constant ["Peano"] "le")
-let coq_gt = lazy (constant ["Peano"] "gt")
+let coq_le = lazy (constant ["Init";"Peano"] "le")
+let coq_gt = lazy (constant ["Init";"Peano"] "gt")
 
 (* Datatypes *)
-let coq_nat = lazy (constant ["Datatypes"] "nat")
-let coq_S = lazy (constant ["Datatypes"] "S")
-let coq_O = lazy (constant ["Datatypes"] "O")
+let coq_nat = lazy (constant ["Init";"Datatypes"] "nat")
+let coq_S = lazy (constant ["Init";"Datatypes"] "S")
+let coq_O = lazy (constant ["Init";"Datatypes"] "O")
 
 (* Minus *)
-let coq_minus = lazy (constant ["Minus"] "minus")
+let coq_minus = lazy (constant ["Arith";"Minus"] "minus")
+
+(* Compare_dec *)
+let coq_le_gt_dec = lazy (constant ["Arith";"Compare_dec"] "le_gt_dec")
 
 (* Logic *)
-let coq_eq = lazy (constant ["Logic"] "eq")
-let coq_and = lazy (constant ["Logic"] "and")
-let coq_not = lazy (constant ["Logic"] "not")
-let coq_or = lazy (constant ["Logic"] "or")
-let coq_ex = lazy (constant ["Logic"] "ex")
+let coq_eq = lazy (constant ["Init";"Logic"] "eq")
+let coq_and = lazy (constant ["Init";"Logic"] "and")
+let coq_not = lazy (constant ["Init";"Logic"] "not")
+let coq_or = lazy (constant ["Init";"Logic"] "or")
+let coq_ex = lazy (constant ["Init";"Logic"] "ex")
 
 (* Section paths for unfold *)
-let sp_Zs = path_of_string "#zarith_aux#Zs.cci"
-let sp_Zminus = path_of_string "#zarith_aux#Zminus.cci"
-let sp_Zle = path_of_string "#zarith_aux#Zle.cci"
-let sp_Zgt = path_of_string "#zarith_aux#Zgt.cci"
-let sp_Zge = path_of_string "#zarith_aux#Zge.cci"
-let sp_Zlt = path_of_string "#zarith_aux#Zlt.cci"
-let sp_not = path_of_string "#Logic#not.cci"
+let sp_Zs = path_of_string "Zarith.zarith_aux.Zs"
+let sp_Zminus = path_of_string "Zarith.zarith_aux.Zminus"
+let sp_Zle = path_of_string "Zarith.zarith_aux.Zle"
+let sp_Zgt = path_of_string "Zarith.zarith_aux.Zgt"
+let sp_Zge = path_of_string "Zarith.zarith_aux.Zge"
+let sp_Zlt = path_of_string "Zarith.zarith_aux.Zlt"
+let sp_not = path_of_string "Init.Logic.not"
 
 let mk_var v = mkVar (id_of_string v)
 let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index b3462d8f37..a8250f4900 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -113,7 +113,8 @@ open Proof_type
   the constants are loaded in the environment *)
 
 let constant dir s =
-  Declare.global_absolute_reference (make_path dir (id_of_string s) CCI)
+  Declare.global_absolute_reference
+    (make_path ("ring"::dir) (id_of_string s) CCI)
 
 let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm")
 let coq_Node_vm = lazy (constant ["Quote"] "Node_vm")
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 775724e49a..fccdc3e784 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -26,7 +26,8 @@ let mt_evd = Evd.empty
 let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com
 
 let constant dir s =
-  Declare.global_absolute_reference (make_path dir (id_of_string s) CCI)
+  Declare.global_absolute_reference
+    (make_path ("ring"::dir) (id_of_string s) CCI)
 
 (* Ring_theory *)
 
@@ -84,10 +85,14 @@ let coq_aspolynomial_normalize_ok =
 let coq_apolynomial_normalize_ok = 
   lazy (constant ["Ring_abstract"] "apolynomial_normalize_ok")
 
+let logic_constant dir s =
+  Declare.global_absolute_reference
+    (make_path ("Init"::dir) (id_of_string s) CCI)
+
 (* Logic *)
-let coq_f_equal2 = lazy (constant ["Logic"] "f_equal2")
-let coq_eq = lazy (constant ["Logic"] "eq")
-let coq_eqT = lazy (constant ["Logic_Type"] "eqT")
+let coq_f_equal2 = lazy (logic_constant ["Logic"] "f_equal2")
+let coq_eq = lazy (logic_constant ["Logic"] "eq")
+let coq_eqT = lazy (logic_constant ["Logic_Type"] "eqT")
 
 (*********** Useful types and functions ************)
 
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index df79fe3f7f..62f7020a1e 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -847,7 +847,7 @@ and print_node n id sp bprintleaf dn =
        end ;
       print_if_verbose "/ClosedDir\n"
    | L.Module s ->
-      print_if_verbose ("Module " ^ s ^ "\n")
+      print_if_verbose ("Module " ^ (Names.string_of_dirpath s) ^ "\n")
    | L.FrozenState _ ->
       print_if_verbose ("FrozenState\n")
 ;;