From 0e025b3b18b545efecfea96f135ad177bb38ced6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 23 Nov 2000 15:11:09 +0000
Subject: Simplification de l'accès aux globaux

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@933 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/ring/quote.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 3a431bc765..8ebd8dc613 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -112,14 +112,14 @@ 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 coq_Empty_vm = lazy (constant "#Quote#varmap.cci" "Empty_vm")
-let coq_Node_vm = lazy (constant "#Quote#varmap.cci" "Node_vm")
-let coq_varmap_find = lazy (constant "#Quote#varmap_find.cci" "varmap_find")
-let coq_Right_idx = lazy (constant "#Quote#index.cci" "Right_idx")
-let coq_Left_idx = lazy (constant "#Quote#index.cci" "Left_idx")
-let coq_End_idx = lazy (constant "#Quote#index.cci" "End_idx")
+let constant dir s = Declare.global_qualified_reference (make_qualid dir s)
+
+let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm")
+let coq_Node_vm = lazy (constant ["Quote"] "Node_vm")
+let coq_varmap_find = lazy (constant ["Quote"] "varmap_find")
+let coq_Right_idx = lazy (constant ["Quote"] "Right_idx")
+let coq_Left_idx = lazy (constant ["Quote"] "Left_idx")
+let coq_End_idx = lazy (constant ["Quote"] "End_idx")
 
 (*s Then comes the stuff to decompose the body of interpetation function
   and pre-compute the inversion data.
-- 
cgit v1.2.3