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.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index db9b00c38..f4848c729 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -36,7 +36,7 @@ open Nametab
open Quote
let mt_evd = Evd.empty
-let constr_of c = Astterm.interp_constr mt_evd (Global.env()) c
+let constr_of c = Constrintern.interp_constr mt_evd (Global.env()) c
let constant dir s =
let dir = make_dirpath (List.map id_of_string (List.rev ("Coq"::dir))) in