diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-10-07 15:17:58 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-10-07 15:19:45 +0200 |
| commit | 8b257187f9b7ec95017a2df14b49c057d254ad15 (patch) | |
| tree | fe770868ede02aedfdd466eacb5296b2657f4c1e | |
| parent | ef7b099bb91ac53770aab886a2051e0c1a1cd056 (diff) | |
Build unfolded versions of the primitive projection in let (a, p) := ...
to maintain compatibility (HoTT bug #557).
| -rw-r--r-- | pretyping/indrec.ml | 6 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
2 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 6e32d70c0..d566dd9b2 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -104,8 +104,10 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = | None -> mkCase (ci, lift ndepar p, mkRel 1, Termops.rel_vect ndepar k) | Some ps -> - let term = mkApp (mkRel 2, - Array.map (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in + let term = + mkApp (mkRel 2, + Array.map + (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in if dep then let ty = mkApp (mkRel 3, [| mkRel 1 |]) in mkCast (term, DEFAULTcast, ty) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b20af031d..5383101b4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -707,7 +707,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var let rec aux n k names l = match names, l with | na :: names, ((_, None, t) :: l) -> - let proj = Projection.make ps.(cs.cs_nargs - k) false in + let proj = Projection.make ps.(cs.cs_nargs - k) true in (na, Some (lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val))), t) :: aux (n+1) (k + 1) names l | na :: names, ((_, c, t) :: l) -> |