diff options
| author | herbelin | 2000-11-22 21:32:03 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-22 21:32:03 +0000 |
| commit | 937ca7a6dbc1a031b7c4540c665b8774440c1bb9 (patch) | |
| tree | 3a2c73669cb40011c2e62a11d3364d39f74040ba /contrib | |
| parent | de9150e6033467fd2fa8fc93d5f057e8c2f6537f (diff) | |
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 'section_path' pour les noms absolus
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/omega/coq_omega.ml | 4 | ||||
| -rw-r--r-- | contrib/ring/quote.ml | 8 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 3 |
3 files changed, 4 insertions, 11 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index bdf4544f95..3b2dff70d9 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -207,9 +207,7 @@ 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 id = - Declare.global_qualified_reference - (make_path dir (id_of_string id) CCI) +let constant dir s = Declare.global_qualified_reference (make_qualid dir s) (* fast_integer *) let coq_xH = lazy (constant ["fast_integer"] "xH") diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 7aba0db663..3a431bc765 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -112,12 +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 sp id = - Declare.global_qualified_reference - (make_path (dirpath (path_of_string sp)) (id_of_string id) CCI) -(* - Declare.global_sp_reference (path_of_string sp) (id_of_string id) -*) +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") diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 6080d7897e..7b96983a7d 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -25,8 +25,7 @@ open Quote;; let mt_evd = Evd.empty let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com -let constant dir id = - Declare.global_qualified_reference (make_path dir (id_of_string id) CCI) +let constant dir s = Declare.global_qualified_reference (make_qualid dir s) (* Ring_theory *) |