Move type_scope into user space, fix some output logs

1 files changed, 5 insertions, 4 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 075e04cba..8395f7d9a 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