diff options
| -rw-r--r-- | pretyping/recordops.ml | 9 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_9375.v | 16 |
2 files changed, 24 insertions, 1 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 6e3b19ae61..f58cce41cc 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -202,7 +202,14 @@ let cs_pattern_of_constr env t = App (f,vargs) -> begin try Const_cs (global_of_constr f) , None, Array.to_list vargs - with e when CErrors.noncritical e -> raise Not_found + with + | Not_found when isProj f -> + let p, c = destProj f in + let { Environ.uj_type = ty } = Typeops.infer env c in + let _, params = Inductive.find_rectype env ty in + Const_cs (ConstRef (Projection.constant p)), None, + params @ [c] @ Array.to_list vargs + | e when CErrors.noncritical e -> raise Not_found end | Rel n -> Default_cs, Some n, [] | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] diff --git a/test-suite/bugs/closed/bug_9375.v b/test-suite/bugs/closed/bug_9375.v new file mode 100644 index 0000000000..a2bfbafe06 --- /dev/null +++ b/test-suite/bugs/closed/bug_9375.v @@ -0,0 +1,16 @@ +Set Primitive Projections. + +Record toto : Type := Toto { + toto1 : Type; + toto2 : toto1 -> Type +}. + +Record tata := Tata { + tata1 : Type +}. + +Canonical Structure tata_toto (x : toto) X := + Tata (toto2 x X). + +Check fun (T : toto) (t : toto1 T) => + (eq_refl _ : @tata1 _ = @toto2 _ t). |