1 files changed, 25 insertions, 0 deletions
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 00000000..1ba8e5c3
--- /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 *)