Commit 97f5318c authored by Janno's avatar Janno

Add type annotations to `sigT` occurrences for 8.7.

parent bb4f6965
......@@ -385,7 +385,8 @@ Fixpoint env_lookup_by_val {A} (P : A) Γ : M ident :=
| Enil => M.raise NotFoundInEnv
end.
Definition envs_lookup_by_val_in {A} P (Δ : envs A) (b : bool) : M { i & envs_lookup i Δ = Some (b,P)} :=
Definition envs_lookup_by_val_in {A} P (Δ : envs A) (b : bool) :
M { i : ident & envs_lookup i Δ = Some (b,P)} :=
let (Γp, Γs) := Δ in
i <- env_lookup_by_val P (if b then Γp else Γs);
(* We could be smarter here for [b = true] but I don't suspect this version to
......@@ -394,7 +395,8 @@ Definition envs_lookup_by_val_in {A} P (Δ : envs A) (b : bool) : M { i & envs_l
e <- M.coerce (eq_refl (Some (b,P)));
M.ret (existT i e).
Definition envs_lookup_by_val {A} P (Δ : envs A): M { b & { i & envs_lookup i Δ = Some (b,P)}} :=
Definition envs_lookup_by_val {A} P (Δ : envs A):
M { b : bool & { i : ident & envs_lookup i Δ = Some (b,P)}} :=
mtry
r <- envs_lookup_by_val_in P Δ true;
M.ret (existT true r)
......
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