aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarconv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarconv.ml')
-rw-r--r--pretyping/evarconv.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index edc948eb65..a82eff9cf0 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -263,7 +263,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
lookup_canonical_conversion
(proji, Sort_cs (Sorts.family s)),[]
| Proj (p, c) ->
- let c2 = Globnames.ConstRef (Projection.constant p) in
+ let c2 = GlobRef.ConstRef (Projection.constant p) in
let c = Retyping.expand_projection env sigma p c [] in
let _, args = destApp sigma c in
let sk2 = Stack.append_app args sk2 in