Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de printers dans ocamldebug

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6554 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 0 insertions, 822 deletions

diff --git a/interp/symbols.ml b/interp/symbols.ml
deleted file mode 100644
index 60e16e709..000000000
--- a/interp/symbols.ml
+++ /dev/null
@@ -1,662 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
-
-(*i*)
-open Util
-open Pp
-open Bigint
-open Names
-open Nametab
-open Libnames
-open Summary
-open Rawterm
-open Topconstr
-open Ppextend
-(*i*)
-
-(*s A scope is a set of notations; it includes
-
-  - a set of ML interpreters/parsers for positive (e.g. 0, 1, 15, ...) and
-    negative numbers (e.g. -0, -2, -13, ...). These interpreters may
-    fail if a number has no interpretation in the scope (e.g. there is
-    no interpretation for negative numbers in [nat]); interpreters both for
-    terms and patterns can be set; these interpreters are in permanent table
-    [numeral_interpreter_tab]
-  - a set of ML printers for expressions denoting numbers parsable in 
-    this scope (permanently declared in [Esyntax.primitive_printer_tab])
-  - a set of interpretations for infix (more generally distfix) notations
-  - an optional pair of delimiters which, when occurring in a syntactic
-    expression, set this scope to be the current scope
-*)
-
-(**********************************************************************)
-(* Scope of symbols *)
-
-type level = precedence * tolerability list
-type delimiters = string
-
-type scope = {
-  notations: (interpretation * (dir_path * string) * bool) Stringmap.t;
-  delimiters: delimiters option
-}
-
-(* Uninterpreted notation map: notation -> level * dir_path *)
-let notation_level_map = ref Stringmap.empty
-
-(* Scopes table: scope_name -> symbol_interpretation *)
-let scope_map = ref Stringmap.empty
-
-let empty_scope = {
-  notations = Stringmap.empty;
-  delimiters = None
-}
-
-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 := Stringmap.add default_scope empty_scope !scope_map;
-  scope_map := Stringmap.add type_scope empty_scope !scope_map
-
-(**********************************************************************)
-(* Operations on scopes *)
-
-let declare_scope scope =
-  try let _ = Stringmap.find scope !scope_map in ()
-  with Not_found ->
-(*    Options.if_verbose message ("Creating scope "^scope);*)
-    scope_map := Stringmap.add scope empty_scope !scope_map
-
-let find_scope scope =
-  try Stringmap.find scope !scope_map
-  with Not_found -> error ("Scope "^scope^" is not declared")
-
-let check_scope sc = let _ = find_scope sc in ()
-
-(**********************************************************************)
-(* The global stack of scopes                                         *)
-
-type scope_elem = Scope of scope_name | SingleNotation of string
-type scopes = scope_elem list
-
-let scope_stack = ref []
-
-let current_scopes () = !scope_stack
-
-(* TODO: push nat_scope, z_scope, ... in scopes summary *)
-
-(* Exportation of scopes *)
-let cache_scope (_,(local,op,sc)) =
-  (match sc with Scope sc -> check_scope sc | _ -> ());
-  scope_stack := if op then sc :: !scope_stack else list_except sc !scope_stack
-
-let subst_scope (_,subst,sc) = sc
-
-open Libobject
-
-let classify_scope (_,(local,_,_ as o)) =
-  if local then Dispose else Substitute o
-
-let export_scope (local,_,_ as x) = if local then None else Some x
-
-let (inScope,outScope) = 
-  declare_object {(default_object "SCOPE") with
-      cache_function = cache_scope;
-      open_function = (fun i o -> if i=1 then cache_scope o);
-      subst_function = subst_scope;
-      classify_function = classify_scope;
-      export_function = export_scope }
-
-let open_close_scope (local,opening,sc) =
-  Lib.add_anonymous_leaf (inScope (local,opening,Scope sc))
-
-let empty_scope_stack = []
-
-let push_scope sc scopes = Scope sc :: scopes
-
-(**********************************************************************)
-(* Delimiters *)
-
-let delimiters_map = ref Stringmap.empty
-
-let declare_delimiters scope key =
-  let sc = find_scope scope in
-  if sc.delimiters <> None && Options.is_verbose () then begin
-    let old = out_some sc.delimiters in
-    Options.if_verbose 
-      warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
-  end;
-  let sc = { sc with delimiters = Some key } in
-  scope_map := Stringmap.add scope sc !scope_map;
-  if Stringmap.mem key !delimiters_map then begin
-    let oldsc = Stringmap.find key !delimiters_map in
-    Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
-  end;
-  delimiters_map := Stringmap.add key scope !delimiters_map
-
-let find_delimiters_scope loc key = 
-  try Stringmap.find key !delimiters_map
-  with Not_found -> 
-    user_err_loc 
-    (loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
-
-(* Uninterpretation tables *)
-
-type interp_rule =
-  | NotationRule of scope_name option * notation
-  | SynDefRule of kernel_name
-
-(* We define keys for rawterm and aconstr to split the syntax entries
-   according to the key of the pattern (adapted from Chet Murthy by HH) *)
-
-type key =
-  | RefKey of global_reference
-  | Oth
-
-(* Scopes table : interpretation -> scope_name *)
-let notations_key_table = ref Gmapl.empty
-let numeral_key_table = Hashtbl.create 7
-
-let rawconstr_key = function
-  | RApp (_,RRef (_,ref),_) -> RefKey ref
-  | RRef (_,ref) -> RefKey ref
-  | _ -> Oth
-
-let cases_pattern_key = function
-  | PatCstr (_,ref,_,_) -> RefKey (ConstructRef ref)
-  | _ -> Oth
-
-let aconstr_key = function
-  | AApp (ARef ref,args) -> RefKey ref, Some (List.length args)
-  | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey ref, Some (List.length args)
-  | ARef ref -> RefKey ref, Some 0
-  | _ -> Oth, None
-
-let pattern_key = function
-  | PatCstr (_,cstr,_,_) -> RefKey (ConstructRef cstr)
-  | _ -> Oth
-
-(**********************************************************************)
-(* Interpreting numbers (not in summary because functional objects)   *)
-
-type num_interpreter =
-    (loc -> bigint -> rawconstr)
-    * (loc -> bigint -> name -> cases_pattern) option
-
-type num_uninterpreter =
-    rawconstr list * (rawconstr -> bigint option)
-    * (cases_pattern -> bigint option) option
-
-type required_module = global_reference * string list 
-
-let numeral_interpreter_tab =
-  (Hashtbl.create 7 : (scope_name,required_module*num_interpreter) Hashtbl.t)
-
-let declare_numeral_interpreter sc dir interp (patl,uninterp,uninterpc) =
-  declare_scope sc;
-  Hashtbl.add numeral_interpreter_tab sc (dir,interp);
-  List.iter
-    (fun pat -> Hashtbl.add numeral_key_table (rawconstr_key pat)
-      (sc,uninterp,uninterpc))
-    patl
-
-let check_required_module loc sc (ref,d) =
-  let d' = List.map id_of_string d in
-  let dir = make_dirpath (List.rev d') in
-  try let _ = sp_of_global ref in ()
-  with Not_found ->
-    user_err_loc (loc,"numeral_interpreter",
-    str ("Cannot interpret numbers in "^sc^" without requiring first module "
-    ^(list_last d)))
-
-let lookup_numeral_interpreter loc = function
-  | Scope sc ->
-      let (dir,interpreter) = Hashtbl.find numeral_interpreter_tab sc in
-      check_required_module loc sc dir;
-      interpreter
-  | SingleNotation _ -> raise Not_found
-
-(* Look if some notation or numeral printer in [scope] can be used in
-   the scope stack [scopes], and if yes, using delimiters or not *)
-
-let find_with_delimiters = function
-  | None -> None
-  | Some scope ->
-      match (Stringmap.find scope !scope_map).delimiters with
-	| Some key -> Some (Some scope, Some key)
-	| None -> None
-
-let rec find_without_delimiters find (ntn_scope,ntn) = function
-  | Scope scope :: scopes -> 
-      (* Is the expected ntn/numpr attached to the most recently open scope? *)
-      if Some scope = ntn_scope then
-	Some (None,None)
-      else
-	(* If the most recently open scope has a notation/numeral printer
-    	   but not the expected one then we need delimiters *)
-	if find scope then
-	  find_with_delimiters ntn_scope
-	else
-	  find_without_delimiters find (ntn_scope,ntn) scopes
-  | SingleNotation ntn' :: scopes ->
-      if ntn_scope = None & ntn = Some ntn' then 
-	Some (None,None)
-      else
-	find_without_delimiters find (ntn_scope,ntn) scopes
-  | [] ->
-      (* Can we switch to [scope]? Yes if it has defined delimiters *)
-      find_with_delimiters ntn_scope
-
-(* Uninterpreted notation levels *)
-
-let declare_notation_level ntn level =
-  if not !Options.v7 & Stringmap.mem ntn !notation_level_map then
-    error ("Notation "^ntn^" is already assigned a level");
-  notation_level_map := Stringmap.add ntn level !notation_level_map
-
-let level_of_notation ntn =
-  Stringmap.find ntn !notation_level_map
-
-(* The mapping between notations and their interpretation *)
-
-let declare_notation_interpretation ntn scopt pat df pp8only =
-  let scope = match scopt with Some s -> s | None -> default_scope in
-  let sc = find_scope scope in
-  if Stringmap.mem ntn sc.notations && Options.is_verbose () then
-    warning ("Notation "^ntn^" was already used"^
-    (if scopt = None then "" else " in scope "^scope));
-  let sc = { sc with notations = Stringmap.add ntn (pat,df,pp8only) sc.notations } in
-  scope_map := Stringmap.add scope sc !scope_map;
-  if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack
-
-let declare_uninterpretation rule (metas,c as pat) =
-  let (key,n) = aconstr_key c in
-  notations_key_table := Gmapl.add key (rule,pat,n) !notations_key_table
-
-let rec find_interpretation f = function
-  | sce :: scopes ->
-      let scope = match sce with
-	| Scope s -> s 
-	| SingleNotation _ -> default_scope in
-      (try f scope
-      with Not_found -> find_interpretation f scopes)
-  | [] -> raise Not_found
-
-let rec interp_notation loc ntn scopes =
-  let f sc =
-    let scope = find_scope sc in
-    let (pat,df,pp8only) = Stringmap.find ntn scope.notations in
-    if pp8only then raise Not_found;
-    pat,(df,if sc = default_scope then None else Some sc) in
-  try find_interpretation f (List.fold_right push_scope scopes !scope_stack)
-  with Not_found -> 
-    user_err_loc
-      (loc,"",str ("Unknown interpretation for notation \""^ntn^"\""))
-
-let uninterp_notations c =
-  Gmapl.find (rawconstr_key c) !notations_key_table
-
-let uninterp_cases_pattern_notations c =
-  Gmapl.find (cases_pattern_key c) !notations_key_table
-
-let availability_of_notation (ntn_scope,ntn) scopes =
-  let f scope =
-    Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
-  find_without_delimiters f (ntn_scope,Some ntn) scopes
-
-let rec interp_numeral_gen loc f n = function
-  | scope :: scopes ->
-      (try f (lookup_numeral_interpreter loc scope)
-       with Not_found -> interp_numeral_gen loc f n scopes)
-  | [] ->
-      user_err_loc (loc,"interp_numeral",
-      str "No interpretation for numeral " ++ pr_bigint n)
-
-let interp_numeral loc n scopes =
-  interp_numeral_gen loc (fun x -> fst x loc n) n
-    (List.fold_right push_scope scopes !scope_stack)
-
-let interp_numeral_as_pattern loc n name scopes =
-  let f x = match snd x with
-    | None -> raise Not_found
-    | Some g -> g loc n name in
-  interp_numeral_gen loc f n (List.fold_right push_scope scopes !scope_stack)
-
-let uninterp_numeral c =
-  try 
-    let (sc,numpr,_) = Hashtbl.find numeral_key_table (rawconstr_key c) in
-    match numpr c with
-      | None -> raise No_match
-      | Some n -> (sc,n)
-  with Not_found -> raise No_match
-
-let uninterp_cases_numeral c =
-  try 
-    match Hashtbl.find numeral_key_table (pattern_key c) with
-      | (_,_,None) -> raise No_match
-      | (sc,_,Some numpr) ->
-	  match numpr c with
-	    | None -> raise No_match
-	    | Some n -> (sc,n)
-  with Not_found -> raise No_match
-
-let availability_of_numeral printer_scope scopes =
-  let f scope = Hashtbl.mem numeral_interpreter_tab scope in
-  option_app snd (find_without_delimiters f (Some printer_scope,None) scopes)
-
-(* Miscellaneous *)
-
-let exists_notation_in_scope scopt ntn r =
-  let scope = match scopt with Some s -> s | None -> default_scope in
-  try
-    let sc = Stringmap.find scope !scope_map in
-    let (r',_,pp8only) = Stringmap.find ntn sc.notations in
-    r' = r, pp8only
-  with Not_found -> false, false
-
-(* Special scopes associated to arguments of a global reference *)
-
-let arguments_scope = ref Refmap.empty
-
-let cache_arguments_scope (_,(r,scl)) =
-  List.iter (option_iter check_scope) scl;
-  arguments_scope := Refmap.add r scl !arguments_scope
-
-let subst_arguments_scope (_,subst,(r,scl)) = (subst_global subst r,scl)
-
-let (inArgumentsScope,outArgumentsScope) = 
-  declare_object {(default_object "ARGUMENTS-SCOPE") with
-      cache_function = cache_arguments_scope;
-      load_function = (fun _ o -> cache_arguments_scope o);
-      subst_function = subst_arguments_scope;
-      classify_function = (fun (_,o) -> Substitute o);
-      export_function = (fun x -> Some x) }
-
-let declare_arguments_scope r scl =
-  Lib.add_anonymous_leaf (inArgumentsScope (r,scl))
-
-let find_arguments_scope r =
-  try Refmap.find r !arguments_scope
-  with Not_found -> []
-
-(**********************************************************************)
-(* Mapping classes to scopes *)
-
-open Classops
-
-let class_scope_map = ref (Gmap.empty : (cl_typ,scope_name) Gmap.t)
-
-let _ = Gmap.add CL_SORT "type_scope" Gmap.empty
-
-let declare_class_scope sc cl =
-  class_scope_map := Gmap.add cl sc !class_scope_map
-
-let find_class_scope cl =
-  Gmap.find cl !class_scope_map
-
-open Term
-
-let find_class t =
-  let t, _ = decompose_app (Reductionops.whd_betaiotazeta t) in
-  match kind_of_term t with
-    | Var id -> CL_SECVAR id
-    | Const sp -> CL_CONST sp
-    | Ind ind_sp -> CL_IND ind_sp
-    | Prod (_,_,_) -> CL_FUN
-    | Sort _ -> CL_SORT
-    |  _ -> raise Not_found
-
-let rec compute_arguments_scope t =
-  match kind_of_term (Reductionops.whd_betaiotazeta t) with
-    | Prod (_,t,u) ->
-	let sc =
-	  try Some (find_class_scope (find_class t)) with Not_found -> None in
-	sc :: compute_arguments_scope u
-    | _ -> []
-
-let declare_ref_arguments_scope ref =
-  let t = Global.type_of_global ref in
-  declare_arguments_scope ref (compute_arguments_scope t)
-
-(********************************)
-(* Encoding notations as string *)
-
-type symbol =
-  | Terminal of string
-  | NonTerminal of identifier
-  | SProdList of identifier * symbol list
-  | Break of int
-
-let rec string_of_symbol = function
-  | NonTerminal _ -> ["_"]
-  | Terminal s -> [s]
-  | SProdList (_,l) -> 
-     let l = List.flatten (List.map string_of_symbol l) in "_"::l@".."::l@["_"]
-  | Break _ -> []
-
-let make_notation_key symbols =
-  String.concat " " (List.flatten (List.map string_of_symbol symbols))
-
-let decompose_notation_key s =
-  let len = String.length s in
-  let rec decomp_ntn dirs n =
-    if n>=len then dirs else
-    let pos =
-      try
-	String.index_from s n ' ' 
-      with Not_found -> len
-    in
-    let tok =
-      match String.sub s n (pos-n) with
-      | "_" -> NonTerminal (id_of_string "_")
-      | s -> Terminal s in
-    decomp_ntn (tok::dirs) (pos+1)	  
-  in
-    decomp_ntn [] 0
-
-(************)
-(* Printing *)
-
-let pr_delimiters_info = function
-  | None -> str "No delimiting key"
-  | Some key -> str "Delimiting key is " ++ str key
-
-let classes_of_scope sc =
-  Gmap.fold (fun cl sc' l -> if sc = sc' then cl::l else l) !class_scope_map []
-
-let pr_scope_classes sc =
-  let l = classes_of_scope sc in
-  if l = [] then mt()
-  else 
-    hov 0 (str ("Bound to class"^(if List.tl l=[] then "" else "es")) ++
-      spc() ++ prlist_with_sep spc pr_class l) ++ fnl()
-
-let rec rawconstr_of_aconstr () x =
-  rawconstr_of_aconstr_with_binders dummy_loc (fun id () -> (id,())) 
-    rawconstr_of_aconstr () x
-
-let pr_notation_info prraw ntn c =
-  str "\"" ++ str ntn ++ str "\" := " ++ prraw (rawconstr_of_aconstr () c)
-
-let pr_named_scope prraw scope sc =
- (if scope = default_scope then
-   match Stringmap.fold (fun _ _ x -> x+1) sc.notations 0 with
-     | 0 -> str "No lonely notation"
-     | n -> str "Lonely notation" ++ (if n=1 then mt() else str"s")
-  else 
-    str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
-  ++ fnl ()
-  ++ pr_scope_classes scope
-  ++ Stringmap.fold
-       (fun ntn ((_,r),(_,df),_) strm ->
-	 pr_notation_info prraw df r ++ fnl () ++ strm)
-       sc.notations (mt ())
-
-let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
-
-let pr_scopes prraw =
- Stringmap.fold 
-   (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
-   !scope_map (mt ())
-
-let rec find_default ntn = function
-  | Scope scope::_ when Stringmap.mem ntn (find_scope scope).notations ->
-      Some scope
-  | SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope
-  | _::scopes -> find_default ntn scopes
-  | [] -> None
-
-let factorize_entries = function
-  | [] -> []
-  | (ntn,c)::l ->
-      let (ntn,l_of_ntn,rest) =
-	List.fold_left
-          (fun (a',l,rest) (a,c) ->
-	    if a = a' then (a',c::l,rest) else (a,[c],(a',l)::rest))
-	  (ntn,[c],[]) l in
-      (ntn,l_of_ntn)::rest
-
-let is_ident s = (* Poor analysis *)
-  String.length s <> 0 & is_letter s.[0]
-
-let browse_notation ntn map =
-  let find =
-    if String.contains ntn ' ' then (=) ntn
-    else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in
-  let l =
-    Stringmap.fold 
-      (fun scope_name sc ->
-	Stringmap.fold (fun ntn ((_,r),df,_) l ->
-	  if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
-      map [] in
-  let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in
-  factorize_entries l
-
-let locate_notation prraw ntn =
-  let ntns = browse_notation ntn !scope_map in
-  if ntns = [] then
-    str "Unknown notation"
-  else
-    t (str "Notation            " ++
-    tab () ++ str "Scope     " ++ tab () ++ fnl () ++ 
-    prlist (fun (ntn,l) ->
-      let scope = find_default ntn !scope_stack in
-      prlist 
-	(fun (sc,r,(_,df)) ->
-	  hov 0 (
-	    pr_notation_info prraw df r ++ tbrk (1,2) ++
-	    (if sc = default_scope then mt () else (str ": " ++ str sc)) ++ 
-	    tbrk (1,2) ++
-	    (if Some sc = scope then str "(default interpretation)" else mt ())
-	    ++ fnl ()))
-	l) ntns)
-
-let collect_notation_in_scope scope sc known =
-  assert (scope <> default_scope);
-  Stringmap.fold
-    (fun ntn ((_,r),(_,df),_) (l,known as acc) ->
-      if List.mem ntn known then acc else ((df,r)::l,ntn::known))
-    sc.notations ([],known)
-
-let collect_notations stack =
-  fst (List.fold_left
-    (fun (all,knownntn as acc) -> function
-      | Scope scope ->
-	  if List.mem_assoc scope all then acc
-	  else
-	    let (l,knownntn) =
-	      collect_notation_in_scope scope (find_scope scope) knownntn in
-	    ((scope,l)::all,knownntn)
-      | SingleNotation ntn ->
-	  if List.mem ntn knownntn then (all,knownntn)
-	  else
-	    let ((_,r),(_,df),_) =
-	      Stringmap.find ntn (find_scope default_scope).notations in
-	    let all' = match all with
-	      | (s,lonelyntn)::rest when s = default_scope ->
-		  (s,(df,r)::lonelyntn)::rest
-	      | _ -> 
-		  (default_scope,[df,r])::all in
-	    (all',ntn::knownntn))
-    ([],[]) stack)
-
-let pr_visible_in_scope prraw (scope,ntns) =
-  let strm =
-    List.fold_right
-      (fun (df,r) strm -> pr_notation_info prraw df r ++ fnl () ++ strm)
-      ntns (mt ()) in
-  (if scope = default_scope then
-     str "Lonely notation" ++ (if List.length ntns <> 1 then str "s" else mt())
-   else 
-     str "Visible in scope " ++ str scope)
-  ++ fnl () ++ strm
-
-let pr_scope_stack prraw stack = 
-  List.fold_left
-    (fun strm scntns -> strm ++ pr_visible_in_scope prraw scntns ++ fnl ())
-    (mt ()) (collect_notations stack)
-
-let pr_visibility prraw = function
-  | Some scope -> pr_scope_stack prraw (push_scope scope !scope_stack)
-  | None -> pr_scope_stack prraw !scope_stack
-
-(**********************************************************************)
-(* Mapping notations to concrete syntax *)
-
-type unparsing_rule = unparsing list * precedence
-
-(* Concrete syntax for symbolic-extension table *)
-let printing_rules = 
-  ref (Stringmap.empty : unparsing_rule Stringmap.t)
-
-let declare_notation_printing_rule ntn unpl =
-  printing_rules := Stringmap.add ntn unpl !printing_rules
-
-let find_notation_printing_rule ntn =
-  try Stringmap.find ntn !printing_rules
-  with Not_found -> anomaly ("No printing rule found for "^ntn)
-
-(**********************************************************************)
-(* Synchronisation with reset *)
-
-let freeze () =
- (!scope_map, !notation_level_map, !scope_stack, !arguments_scope,
-  !delimiters_map, !notations_key_table, !printing_rules,
-  !class_scope_map)
-
-let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
-  scope_map := scm;
-  notation_level_map := nlm;
-  scope_stack := scs;
-  delimiters_map := dlm;
-  arguments_scope := asc;
-  notations_key_table := fkm;
-  printing_rules := pprules;
-  class_scope_map := clsc
-
-let init () =
-  init_scope_map ();
-(*
-  scope_stack := Stringmap.empty
-  arguments_scope := Refmap.empty
-*)
-  notation_level_map := Stringmap.empty;
-  delimiters_map := Stringmap.empty;
-  notations_key_table := Gmapl.empty;
-  printing_rules := Stringmap.empty;
-  class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
-
-let _ = 
-  declare_summary "symbols"
-    { freeze_function = freeze;
-      unfreeze_function = unfreeze;
-      init_function = init;
-      survive_module = false;
-      survive_section = false }
diff --git a/interp/symbols.mli b/interp/symbols.mli
deleted file mode 100644
index e803d65e7..000000000
--- a/interp/symbols.mli
+++ /dev/null
@@ -1,160 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
-
-(*i*)
-open Util
-open Pp
-open Bigint
-open Names
-open Nametab
-open Libnames
-open Rawterm
-open Topconstr
-open Ppextend
-
-(*i*)
-
-(**********************************************************************)
-(* Scopes *)
-
-(*s A scope is a set of interpreters for symbols + optional
-   interpreter and printers for integers + optional delimiters *)
-
-type level = precedence * tolerability list
-type delimiters = string
-type scope
-type scopes (* = scope_name list*)
-
-val type_scope : scope_name
-val declare_scope : scope_name -> unit
-
-(* Open scope *)
-
-val current_scopes : unit -> scopes
-val open_close_scope : 
-  (* locality *) bool * (* open *) bool * scope_name -> unit
-
-(* Extend a list of scopes *)
-val empty_scope_stack : scopes
-val push_scope : scope_name -> scopes -> scopes
-
-(* Declare delimiters for printing *)
-
-val declare_delimiters : scope_name -> delimiters -> unit
-val find_delimiters_scope : loc -> delimiters -> scope_name
-
-(*s Declare and uses back and forth a numeral interpretation *)
-
-(* A numeral interpreter is the pair of an interpreter for _integer_
-   numbers in terms and an optional interpreter in pattern, if
-   negative numbers are not supported, the interpreter must fail with
-   an appropriate error message *)
-
-type num_interpreter =
-    (loc -> bigint -> rawconstr)
-    * (loc -> bigint -> name -> cases_pattern) option
-
-type num_uninterpreter =
-    rawconstr list * (rawconstr -> bigint option)
-    * (cases_pattern -> bigint option) option
-
-type required_module = global_reference * string list 
-val declare_numeral_interpreter : scope_name -> required_module ->
-  num_interpreter -> num_uninterpreter -> unit
-
-(* Returns the term/cases_pattern bound to a numeral in a given scope context*)
-val interp_numeral : loc -> bigint -> scope_name list -> rawconstr
-val interp_numeral_as_pattern : loc -> bigint -> name -> scope_name list ->
-  cases_pattern
-
-(* Returns the numeral bound to a term/cases_pattern; raises No_match if no *)
-(* such numeral *)
-val uninterp_numeral : rawconstr -> scope_name * bigint
-val uninterp_cases_numeral : cases_pattern -> scope_name * bigint
-
-val availability_of_numeral : scope_name -> scopes -> delimiters option option
-
-(*s Declare and interpret back and forth a notation *)
-
-(* Binds a notation in a given scope to an interpretation *)
-type interp_rule =
-  | NotationRule of scope_name option * notation
-  | SynDefRule of kernel_name
-val declare_notation_interpretation : notation -> scope_name option ->
-      interpretation -> dir_path * string -> bool -> unit
-
-val declare_uninterpretation : interp_rule -> interpretation -> unit
-
-(* Returns the interpretation bound to a notation *)
-val interp_notation : loc -> notation -> scope_name list -> 
-      interpretation * ((dir_path * string) * scope_name option)
-
-(* Returns the possible notations for a given term *)
-val uninterp_notations : rawconstr ->
-      (interp_rule * interpretation * int option) list
-val uninterp_cases_pattern_notations : cases_pattern ->
-      (interp_rule * interpretation * int option) list
-
-(* Test if a notation is available in the scopes *)
-(* context [scopes] if available, the result is not None; the first *)
-(* argument is itself not None if a delimiters is needed; the second *)
-(* argument is a numeral printer if the *)
-val availability_of_notation : scope_name option * notation -> scopes -> 
-  (scope_name option * delimiters option) option
-
-(*s Declare and test the level of a (possibly uninterpreted) notation *)
-
-val declare_notation_level : notation -> level option * level -> unit
-val level_of_notation : notation -> level option * level 
-      (* raise [Not_found] if no level *)
-
-(*s** Miscellaneous *)
-
-(* Checks for already existing notations *)
-val exists_notation_in_scope : scope_name option -> notation ->
-      interpretation -> bool * bool
-
-(* Declares and looks for scopes associated to arguments of a global ref *)
-val declare_arguments_scope: global_reference -> scope_name option list -> unit
-val find_arguments_scope : global_reference -> scope_name option list
-
-val declare_class_scope : scope_name -> Classops.cl_typ -> unit
-val declare_ref_arguments_scope : global_reference -> unit
-
-val compute_arguments_scope : Term.types -> scope_name option list
-
-(* Building notation key *)
-
-type symbol =
-  | Terminal of string
-  | NonTerminal of identifier
-  | SProdList of identifier * symbol list
-  | Break of int
-
-val make_notation_key : symbol list -> notation
-val decompose_notation_key : notation -> symbol list
-
-(* Prints scopes (expect a pure aconstr printer *)
-val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
-val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds
-val locate_notation : (rawconstr -> std_ppcmds) -> notation -> std_ppcmds
-
-val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds
-
-(**********************************************************************)
-(*s Printing rules for notations *)
-
-(* Declare and look for the printing rule for symbolic notations *)
-type unparsing_rule = unparsing list * precedence
-val declare_notation_printing_rule : notation -> unparsing_rule -> unit
-val find_notation_printing_rule : notation -> unparsing_rule
-
-(**********************************************************************)
-(* Rem: printing rules for numerals are trivial *)