Commit 7ef2e547 authored by Janno's avatar Janno

Add one more missing type annotation for 8.7.

parent 97f5318c
......@@ -402,7 +402,7 @@ Definition envs_lookup_by_val {A} P (Δ : envs A):
M.ret (existT true r)
with NotFoundInEnv =n>
r <- envs_lookup_by_val_in P Δ false;
M.ret (existT (P:=fun b => { i & _ = Some (b, _)}) false r)
M.ret (existT (P:=fun b => { i : ident & _ = Some (b, _)}) false r)
end.
(* [iAssumptionLookup] is a very flexible tactic that can be used in scenarios where:
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment