diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/ring/quote.ml | 2 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index a8250f490..666d15dee 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -114,7 +114,7 @@ open Proof_type let constant dir s = Declare.global_absolute_reference - (make_path ("ring"::dir) (id_of_string s) CCI) + (make_path ("Coq"::"ring"::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 fccdc3e78..aa7b305c0 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -27,7 +27,7 @@ let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com let constant dir s = Declare.global_absolute_reference - (make_path ("ring"::dir) (id_of_string s) CCI) + (make_path ("Coq"::"ring"::dir) (id_of_string s) CCI) (* Ring_theory *) @@ -87,7 +87,7 @@ let coq_apolynomial_normalize_ok = let logic_constant dir s = Declare.global_absolute_reference - (make_path ("Init"::dir) (id_of_string s) CCI) + (make_path ("Coq"::"Init"::dir) (id_of_string s) CCI) (* Logic *) let coq_f_equal2 = lazy (logic_constant ["Logic"] "f_equal2") |