Imported Upstream version 8.5~beta1+dfsg

1 files changed, 49 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_084.v b/test-suite/bugs/closed/HoTT_coq_084.v
new file mode 100644
index 00000000..d007e4e2
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_084.v
@@ -0,0 +1,49 @@
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Module success.
+  Unset Primitive Projections.
+
+  Record group :=
+    { carrier : Type;
+      id : carrier }.
+
+  Notation "1" := (id _) : g_scope.
+
+  Delimit Scope g_scope with g.
+  Bind Scope g_scope with carrier.
+
+  Section foo.
+    Variable g : group.
+    Variable comp : carrier g -> carrier g -> carrier g.
+
+    Check comp 1 1.
+  End foo.
+End success.
+
+Module failure.
+  Set Primitive Projections.
+
+  Record group :=
+    { carrier : Type;
+      id : carrier }.
+
+  Notation "1" := (id _) : g_scope.
+
+  Delimit Scope g_scope with g.
+  Bind Scope g_scope with carrier.
+
+  Section foo.
+    Variable g : group.
+    Variable comp : carrier g -> carrier g -> carrier g.
+
+    Check comp 1 1.
+    (* Toplevel input, characters 11-12:
+Error:
+In environment
+g : group
+comp : carrier g -> carrier g -> carrier g
+The term "1" has type "nat" while it is expected to have type "carrier g".
+    *)
+  End foo.
+End failure.