From 362e81735b07f96cb87e1203328592fc394beaad Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 17 Jun 2014 15:22:18 +0200
Subject: - Fix the de Bruijn problem in check_projection for good :) - Fix
 HoTT coq bug #80, implicit arguments with primitive projections were wrongly
 automatically infered.

---
 test-suite/bugs/closed/HoTT_coq_080.v | 27 +++++++++++++++++++++++++++
 test-suite/bugs/opened/HoTT_coq_080.v | 34 ----------------------------------
 2 files changed, 27 insertions(+), 34 deletions(-)
 create mode 100644 test-suite/bugs/closed/HoTT_coq_080.v
 delete mode 100644 test-suite/bugs/opened/HoTT_coq_080.v

(limited to 'test-suite')

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
diff --git a/test-suite/bugs/opened/HoTT_coq_080.v b/test-suite/bugs/opened/HoTT_coq_080.v
deleted file mode 100644
index 9f6949d395..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_080.v
+++ /dev/null
@@ -1,34 +0,0 @@
-Set Primitive Projections.
-Set Implicit Arguments.
-Set Universe Polymorphism.
-Set Asymmetric Patterns.
-
-Inductive sum A B := inl : A -> sum A B | inr : B -> sum A B.
-Inductive Empty :=.
-
-Record category :=
-  { ob :> Type;
-    hom : ob -> ob -> Type
-  }.
-Set Printing All.
-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.
-Fail exact (hom x y). (* Toplevel input, characters 26-27:
-Error:
-In environment
-C : category
-D : category
-x : sum (ob C) (ob D)
-y : sum (ob C) (ob D)
-The term "x" has type "sum (ob C) (ob D)" while it is expected to have type
- "ob ?16". *)
-- 
cgit v1.2.3