diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-26 20:43:25 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-26 20:43:25 +0000 |
| commit | 96a64b9be7551b562e0f6d3204a8a1af837a0626 (patch) | |
| tree | 16a34129a30dfd88568216945fa257834099aa8f /contrib | |
| parent | 735070100540076e715792bf17fa291e4a4cbfd5 (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/omega/coq_omega.ml | 3 | ||||
| -rw-r--r-- | contrib/ring/quote.ml | 3 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 3 |
3 files changed, 6 insertions, 3 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 9efa5aa4a..9b3aa0694 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 8ebd8dc61..b3462d8f3 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 d2c379659..775724e49 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 *) |