From 96a64b9be7551b562e0f6d3204a8a1af837a0626 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 26 Nov 2000 20:43:25 +0000
Subject: Appel des constantes globaux par des noms absolus

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@966 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/omega/coq_omega.ml | 3 ++-
 contrib/ring/quote.ml      | 3 ++-
 contrib/ring/ring.ml       | 3 ++-
 tactics/equality.ml        | 3 ++-
 tactics/tactics.ml         | 3 ++-
 5 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 9efa5aa4a5..9b3aa06940 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -211,7 +211,8 @@ let recognize_number t =
  To use the constant Zplus, one must type "Lazy.force coq_Zplus"
  This is the right way to access to Coq constants in tactics ML code *)
 
-let constant dir s = Declare.global_qualified_reference (make_qualid dir s)
+let constant dir s =
+  Declare.global_absolute_reference (make_path dir (id_of_string s) CCI)
 
 (* fast_integer *)
 let coq_xH = lazy (constant ["fast_integer"] "xH")
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 8ebd8dc613..b3462d8f37 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -112,7 +112,8 @@ open Proof_type
   We do that lazily, because this code can be linked before
   the constants are loaded in the environment *)
 
-let constant dir s = Declare.global_qualified_reference (make_qualid dir s)
+let constant dir s =
+  Declare.global_absolute_reference (make_path 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 d2c379659e..775724e49a 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -25,7 +25,8 @@ open Quote;;
 let mt_evd = Evd.empty
 let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com
 
-let constant dir s = Declare.global_qualified_reference (make_qualid dir s)
+let constant dir s =
+  Declare.global_absolute_reference (make_path dir (id_of_string s) CCI)
 
 (* Ring_theory *)
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 96c323d733..83af309491 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -669,7 +669,8 @@ let h_discrHyp   = hide_ident_tactic  "DiscrHyp"   discrHyp
 let existS_pattern = put_pat mmk "(existS ?1 ?2 ?3 ?4)"
 let existT_pattern = put_pat mmk "(existT ?1 ?2 ?3 ?4)"
 
-let constant dir s = Declare.global_qualified_reference (make_qualid dir s)
+let constant dir s =
+  Declare.global_absolute_reference (make_path dir (id_of_string s) CCI)
 
 let build_sigma_set () =
   { proj1 = constant ["Specif"] "projS1";
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6d3da97ad0..cf9946b8e9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1524,7 +1524,8 @@ let contradiction_on_hyp id gl =
   else 
     error "Not a contradiction"
 
-let constant dir s = Declare.global_qualified_reference (make_qualid dir s)
+let constant dir s = 
+  Declare.global_absolute_reference (make_path dir (id_of_string s) CCI)
 
 let coq_False = lazy (constant ["Logic"] "False")
 let coq_not = lazy (constant ["Logic"] "not")
-- 
cgit v1.2.3