From c5ecebf6fefbaa673dda506175a2aa4a69d79807 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 17 Sep 2014 00:03:46 +0200
Subject: Revert specific syntax for primitive projections, avoiding ugly
 contortions in internalization/externalization. It uses a fully typed version
 of detyping, requiring the environment, to move from primitive projection
 applications to regular applications of the eta-expanded version. The kernel
 is unchanged, and only constrMatching needs compatibility code now.

---
 test-suite/bugs/opened/HoTT_coq_083.v | 29 -----------------------------
 1 file changed, 29 deletions(-)
 delete mode 100644 test-suite/bugs/opened/HoTT_coq_083.v

(limited to 'test-suite/bugs/opened')

diff --git a/test-suite/bugs/opened/HoTT_coq_083.v b/test-suite/bugs/opened/HoTT_coq_083.v
deleted file mode 100644
index 0917202721..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_083.v
+++ /dev/null
@@ -1,29 +0,0 @@
-Set Primitive Projections.
-Set Implicit Arguments.
-Set Universe Polymorphism.
-
-Record category :=
-  { ob : Type }.
-
-Goal forall C, ob C -> ob C.
-intros.
-generalize dependent (ob C).
-(* 1 subgoals, subgoal 1 (ID 7)
-
-  C : category
-  ============================
-   forall T : Type, T -> T
-(dependent evars:) *)
-intros T t.
-Undo 2.
-generalize dependent (@ob C).
-(* 1 subgoals, subgoal 1 (ID 6)
-
-  C : category
-  X : ob C
-  ============================
-   Type -> ob C
-(dependent evars:) *)
-Fail intros T t.
-(* Toplevel input, characters 9-10:
-Error: No product even after head-reduction. *)
-- 
cgit v1.2.3