diff options
| author | herbelin | 2005-01-02 08:47:14 +0000 |
|---|---|---|
| committer | herbelin | 2005-01-02 08:47:14 +0000 |
| commit | 2dee039338e6f130447741b67f36eba666131b8a (patch) | |
| tree | b7ac63eb7f7cc87edfa0056e7c69653fd6c802a1 /parsing/esyntax.ml | |
| parent | da705691fc9cf7724f78f4ed0cc8b93c4d7bc08e (diff) | |
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@6546 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/esyntax.ml')
| -rw-r--r-- | parsing/esyntax.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml index 464c1fffd9..1ee900dbcd 100644 --- a/parsing/esyntax.ml +++ b/parsing/esyntax.ml @@ -19,7 +19,7 @@ open Ppextend open Names open Nametab open Topconstr -open Symbols +open Notation (*** Syntax keys ***) @@ -228,7 +228,7 @@ let call_primitive_parser rec_pr otherwise inherited scopes (se,env) = (* Test for a primitive printer; may raise Not_found *) let sc,pr = lookup_primitive_printer c in (* Look if scope [sc] associated to this printer is OK *) - (match Symbols.availability_of_numeral sc scopes with + (match Notation.availability_of_numeral sc scopes with | None -> otherwise () | Some key -> (* We can use this printer *) @@ -237,12 +237,12 @@ let call_primitive_parser rec_pr otherwise inherited scopes (se,env) = | Some strm -> print_delimiters inherited se strm key | None -> otherwise ()) | [UNP_SYMBOLIC (sc,pat,sub)] -> - (match Symbols.availability_of_notation (sc,pat) scopes with + (match Notation.availability_of_notation (sc,pat) scopes with | None -> otherwise () | Some (scopt,key) -> print_delimiters inherited se (print_syntax_entry rec_pr - (option_fold_right Symbols.push_scope scopt scopes) env + (option_fold_right Notation.push_scope scopt scopes) env {se with syn_hunks = [sub]}) key) | _ -> pr_parenthesis inherited se (print_syntax_entry rec_pr scopes env se) @@ -270,7 +270,7 @@ let genprint dflt whatfor inhprec ast = in test_rule entries in try - rec_pr (Symbols.current_scopes ()) inhprec ast + rec_pr (Notation.current_scopes ()) inhprec ast with | Failure _ -> (str"<PP failure: " ++ dflt ast ++ str">") | Not_found -> (str"<PP search failure: " ++ dflt ast ++ str">") |