diff options
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 *) |