diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5c18297c0..8c4dbfd98 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -566,6 +566,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var let app_f = match kind_of_term fj.uj_val with | Const (p, u) when Environ.is_projection p env -> + let p = Projection.make p false in let pb = Environ.lookup_projection p env in let npars = pb.Declarations.proj_npars in fun n -> @@ -705,7 +706,8 @@ 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) -> - (na, Some (lift (cs.cs_nargs - n) (mkProj (ps.(cs.cs_nargs - k), cj.uj_val))), t) + let proj = Projection.make ps.(cs.cs_nargs - k) false 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) -> (na, c, t) :: aux (n+1) k names l |