Move type_scope into user space, fix some output logs

3 files changed, 23 insertions, 1 deletions

diff --git a/test-suite/bugs/closed/3080.v b/test-suite/bugs/closed/3080.v
new file mode 100644
index 000000000..7d0dc090e
--- /dev/null
+++ b/test-suite/bugs/closed/3080.v
@@ -0,0 +1,18 @@
+(* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
+Delimit Scope type_scope with type.
+Delimit Scope function_scope with function.
+
+Bind Scope type_scope with Sortclass.
+Bind Scope function_scope with Funclass.
+
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+
+Definition compose {A B C} (g : B -> C) (f : A -> B) :=
+  fun x : A => g (f x).
+
+Notation " g ∘ f " := (compose g f)
+  (at level 40, left associativity) : function_scope.
+
+Fail Check (fun x => x) ∘ (fun x => x). (* this [Check] should fail, as [function_scope] is not opened *)
+Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arugments to [compose] *)
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index 9125ab16d..324c12525 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -6,6 +6,8 @@ lines, then from 421 lines to 428 lines, then from 444 lines to 429 lines, then
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y  :>  T" (at level 70, y at next level, no associativity).
 Reserved Notation "x = y" (at level 70, no associativity).
+Delimit Scope type_scope with type.
+Bind Scope type_scope with Sortclass.
 Open Scope type_scope.
 Global Set Universe Polymorphism.
 Notation "A -> B" := (forall (_ : A), B) : type_scope.
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index 06188e7b1..fc60897d2 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -4,6 +4,8 @@
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y" (at level 70, no associativity).
+Delimit Scope type_scope with type.
+Bind Scope type_scope with Sortclass.
 Open Scope type_scope.
 Axiom admit : forall {T}, T.
 Notation "A -> B" := (forall (_ : A), B) : type_scope.
@@ -54,4 +56,4 @@ Goal forall (C D : PreCategory) (G G' : Functor C D)
   (** This [change] succeeded, but did not progress, in 07e4438bd758c2ced8caf09a6961ccd77d84e42b, because [T0 x o T1 x] was not found in the goal *)
   let T0 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T0) end in
   let T1 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T1) end in
-  progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)).
\ No newline at end of file
+  progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)).