From d483b7171dafadbe01520bbb6d0c75aa0d6099a7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 16 May 2014 19:25:16 +0200
Subject: Fix unification of non-unfoldable primitive projections in evarconv.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/HoTT_coq_122.v b/test-suite/bugs/closed/HoTT_coq_122.v
new file mode 100644
index 0000000000..1ba8e5c345
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_122.v
@@ -0,0 +1,25 @@
+(* File reduced by coq-bug-finder from original input, then from 669 lines to 79 lines, then from 89 lines to 44 lines *)
+Set Primitive Projections.
+Reserved Notation "g 'o' f" (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Notation "x = y" := (@paths _ x y) : type_scope.
+
+Set Implicit Arguments.
+
+Record PreCategory :=
+  Build_PreCategory' {
+      object :> Type;
+      morphism : object -> object -> Type;
+
+      identity : forall x, morphism x x;
+      compose : forall s d d',
+                  morphism d d'
+                  -> morphism s d
+                  -> morphism s d'
+                              where "f 'o' g" := (compose f g);
+
+      left_identity : forall a b (f : morphism a b), identity b o f = f
+    }.
+
+Hint Rewrite @left_identity. (* stack overflow *)
diff --git a/test-suite/bugs/opened/HoTT_coq_122.v b/test-suite/bugs/opened/HoTT_coq_122.v
deleted file mode 100644
index 7e474d0a12..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_122.v
+++ /dev/null
@@ -1,25 +0,0 @@
-(* File reduced by coq-bug-finder from original input, then from 669 lines to 79 lines, then from 89 lines to 44 lines *)
-Set Primitive Projections.
-Reserved Notation "g 'o' f" (at level 40, left associativity).
-Inductive paths {A : Type} (a : A) : A -> Type :=
-  idpath : paths a a.
-Notation "x = y" := (@paths _ x y) : type_scope.
-
-Set Implicit Arguments.
-
-Record PreCategory :=
-  Build_PreCategory' {
-      object :> Type;
-      morphism : object -> object -> Type;
-
-      identity : forall x, morphism x x;
-      compose : forall s d d',
-                  morphism d d'
-                  -> morphism s d
-                  -> morphism s d'
-                              where "f 'o' g" := (compose f g);
-
-      left_identity : forall a b (f : morphism a b), identity b o f = f
-    }.
-
-Fail Timeout 1 Hint Rewrite @left_identity. (* stack overflow *)
-- 
cgit v1.2.3