Fix HoTT bug #84, binding scopes to projections.

1 files changed, 0 insertions, 49 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_084.v b/test-suite/bugs/opened/HoTT_coq_084.v
deleted file mode 100644
index 5568ec244e..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_084.v
+++ /dev/null
@@ -1,49 +0,0 @@
-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.
-
-    Fail 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.