aboutsummaryrefslogtreecommitdiff
path: root/kernel/csymtable.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/csymtable.ml')
-rw-r--r--kernel/csymtable.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index d81b98ac47..26b997f0f4 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -143,7 +143,7 @@ and slot_for_fv env fv =
match !rv with
| VKvalue (v, _) -> v
| VKnone ->
- let (_, b, _) = Sign.lookup_rel i env.env_rel_context in
+ let (_, b, _) = lookup_rel i env.env_rel_context in
let (v, d) =
match b with
| None -> (val_of_rel i, Idset.empty)