Fix unification of non-unfoldable primitive projections in evarconv.

1 files changed, 0 insertions, 25 deletions

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 *)