aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/ring/ring.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/ring/ring.ml')
-rw-r--r--contrib/ring/ring.ml3
1 files changed, 2 insertions, 1 deletions
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 *)