aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/csymtable.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/csymtable.ml')
-rw-r--r--kernel/csymtable.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 236d83576..a693e62a6 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -150,6 +150,7 @@ and slot_for_fv env fv =
env |> Pre_env.lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel
| Some (v, _) -> v
end
+ | FVevar evk -> val_of_evar evk
| FVuniv_var idu ->
assert false