Add more regression tests for univ poly/prim proj

hese regression tests are aggregated from the various bugs I (and
others) have reported on https://github.com/HoTT/coq/issues relating to
universe polymorphism, primitive projections, and eta for records.

These are the tests that trunk currently fails.

I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the
number of the issue in GitHub), but I couldn't think of a better one.

1 files changed, 25 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_111.v b/test-suite/bugs/closed/HoTT_coq_111.v
new file mode 100644
index 000000000..56feadb40
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_111.v
@@ -0,0 +1,25 @@
+Module X.
+  Set Universe Polymorphism.
+  Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x.
+  Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope.
+
+  Axioms A B : Type.
+  Axiom P : A = B.
+  Definition foo : A = B.
+    abstract (rewrite <- P; reflexivity).
+  (* Error: internal_paths_rew already exists. *)
+  Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+End X.
+
+Module Y.
+  Set Universe Polymorphism.
+  Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x.
+  Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope.
+
+  Axioms A B : Type.
+  Axiom P : A = B.
+  Definition foo : (A = B) * (A = B).
+    split; abstract (rewrite <- P; reflexivity).
+  (* Error: internal_paths_rew already exists. *)
+  Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+End Y.