- Fix the de Bruijn problem in check_projection for good :)

- Fix HoTT coq bug #80, implicit arguments with primitive projections were
wrongly automatically infered.

1 files changed, 27 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_080.v b/test-suite/bugs/closed/HoTT_coq_080.v
new file mode 100644
index 0000000000..6b07c30404
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_080.v
@@ -0,0 +1,27 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Set Asymmetric Patterns.
+Set Printing Projections.
+Inductive sum A B := inl : A -> sum A B | inr : B -> sum A B.
+Inductive Empty :=.
+
+Record category :=
+  { ob :> Type;
+    hom : ob -> ob -> Type
+  }.
+
+Definition sum_category (C D : category) : category :=
+  {|
+    ob := sum (ob C) (ob D);
+    hom x y := match x, y with
+                 | inl x, inl y => @hom C x y
+                 | inr x, inr y => @hom D x y
+                 | _, _ => Empty
+               end |}.
+
+Goal forall C D (x y : ob (sum_category C D)), Type.
+intros C D x y.
+hnf in x, y.
+exact (hom (sum_category _ _) x y). 
+Defined.
\ No newline at end of file