Move type_scope into user space, fix some output logs

8 files changed, 43 insertions, 14 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f57772ecb0..1c60d5c2f7 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -788,7 +788,7 @@ let rec extern inctx scopes vars r =
 	     Miscops.map_cast_type (extern_typ scopes vars) c')
 
 and extern_typ (_,scopes) =
-  extern true (Some Notation.type_scope,scopes)
+  extern true (Notation.current_type_scope_name (),scopes)
 
 and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8c56d0ccfe..d572508a15 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -298,7 +298,7 @@ let set_var_scope loc id istermvar env ntnvars =
     (* Not in a notation *)
     ()
 
-let set_type_scope env = {env with tmp_scope = Some Notation.type_scope}
+let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_name ()}
 
 let reset_tmp_scope env = {env with tmp_scope = None}
 
@@ -449,12 +449,15 @@ let intern_generalization intern env lvar loc bk ak c =
 	| Some AbsPi -> true
         | Some _ -> false
 	| None ->
-          let is_type_scope = match env.tmp_scope with
+          match Notation.current_type_scope_name () with
+          | Some type_scope ->
+              let is_type_scope = match env.tmp_scope with
+              | None -> false
+              | Some sc -> String.equal sc type_scope
+              in
+              is_type_scope ||
+              String.List.mem type_scope env.scopes
           | None -> false
-          | Some sc -> String.equal sc Notation.type_scope
-          in
-          is_type_scope ||
-          String.List.mem Notation.type_scope env.scopes
       in
 	if pi then
 	  (fun (id, loc') acc ->
@@ -1755,7 +1758,7 @@ let extract_ids env =
     Id.Set.empty
 
 let scope_of_type_kind = function
-  | IsType -> Some Notation.type_scope
+  | IsType -> Notation.current_type_scope_name ()
   | OfType typ -> compute_type_scope typ
   | WithoutTypeConstraint -> None
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 075e04cba0..8395f7d9ad 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -65,11 +65,9 @@ let empty_scope = {
 }
 
 let default_scope = "" (* empty name, not available from outside *)
-let type_scope = "type_scope" (* special scope used for interpreting types *)
 
 let init_scope_map () =
-  scope_map := String.Map.add default_scope empty_scope !scope_map;
-  scope_map := String.Map.add type_scope empty_scope !scope_map
+  scope_map := String.Map.add default_scope empty_scope !scope_map
 
 (**********************************************************************)
 (* Operations on scopes *)
@@ -576,7 +574,7 @@ end
 module ScopeClassMap = Map.Make(ScopeClassOrd)
 
 let initial_scope_class_map : scope_name ScopeClassMap.t =
-  ScopeClassMap.add CL_SORT type_scope ScopeClassMap.empty
+  ScopeClassMap.empty
 
 let scope_class_map = ref initial_scope_class_map
 
@@ -610,6 +608,9 @@ let compute_arguments_scope t = fst (compute_arguments_scope_full t)
 let compute_type_scope t =
   find_scope_class_opt (try Some (compute_scope_class t) with Not_found -> None)
 
+let current_type_scope_name () =
+   find_scope_class_opt (Some CL_SORT)
+
 let scope_class_of_class (x : cl_typ) : scope_class =
   x
 
diff --git a/interp/notation.mli b/interp/notation.mli
index 85c4be4cc1..2bfbb33c2d 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -29,7 +29,6 @@ type scopes (** = [scope_name list] *)
 
 type local_scopes = tmp_scope_name option * scope_name list
 
-val type_scope : scope_name
 val declare_scope : scope_name -> unit
 
 val current_scopes : unit -> scopes
@@ -165,6 +164,9 @@ val declare_ref_arguments_scope : global_reference -> unit
 val compute_arguments_scope : Term.types -> scope_name option list
 val compute_type_scope : Term.types -> scope_name option
 
+(** Get the current scope bound to Sortclass, if it exists *)
+val current_type_scope_name : unit -> scope_name option
+
 val scope_class_of_class : Classops.cl_typ -> scope_class
 
 (** Building notation key *)
diff --git a/test-suite/bugs/closed/3080.v b/test-suite/bugs/closed/3080.v
new file mode 100644
index 0000000000..7d0dc090e1
--- /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 9125ab16dd..324c12525c 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 06188e7b1b..fc60897d21 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)).
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 50728136ba..ef6125e6fa 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -79,6 +79,7 @@ Delimit Scope type_scope with type.
 Delimit Scope function_scope with function.
 Delimit Scope core_scope with core.
 
+Bind Scope type_scope with Sortclass.
 Bind Scope function_scope with Funclass.
 
 Open Scope core_scope.