Move type_scope into user space, fix some output logs

4 files changed, 19 insertions, 13 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 *)