diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-23 15:11:09 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-23 15:11:09 +0000 |
| commit | 0e025b3b18b545efecfea96f135ad177bb38ced6 (patch) | |
| tree | d531f966172213aeee24198aa1cdd66d3ef38b38 /contrib/ring | |
| parent | 5b4c144db2e39e7926d1eebac5e3bce50e68550f (diff) | |
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
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/quote.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 3a431bc76..8ebd8dc61 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. |