Réforme de l'interprétation des termes :

- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
  pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
  se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
  constrextern.ml est l'équivalent de termast.ml pour le nouveau
  printer; topconstr.ml; contient la définition de "constr_expr";
  modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid


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

1 files changed, 10 insertions, 7 deletions

diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 1b667918a..fbbe4a94e 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -11,32 +11,35 @@
 (*i*)
 open Util
 open Libnames
+open Ppextend
 open Extend
 open Tacexpr
 open Vernacexpr
 open Symbols
+open Topconstr
 (*i*)
 
 (* Adding grammar and pretty-printing objects in the environment *)
 
-val add_syntax_obj : string -> syntax_entry_ast list -> unit
+val add_syntax_obj : string -> raw_syntax_entry list -> unit
 
-val add_grammar_obj : string -> grammar_entry_ast list -> unit
+val add_grammar_obj : string -> raw_grammar_entry list -> unit
 val add_token_obj : string -> unit
 val add_tactic_grammar :
   (string * (string * grammar_production list) * raw_tactic_expr) list -> unit
 
 val add_infix :
-  Gramext.g_assoc option -> precedence -> string -> qualid located
+  grammar_associativity -> precedence -> string -> reference
     -> scope_name option -> unit
 val add_distfix :
-  Gramext.g_assoc option -> precedence -> string -> Coqast.t 
+  grammar_associativity -> precedence -> string -> reference
     -> scope_name option -> unit
 val add_delimiters : scope_name -> delimiters -> unit
 
-val add_notation : 
-  Gramext.g_assoc option -> precedence -> string -> Coqast.t
-    -> (string * precedence) list -> scope_name option -> unit
+val add_notation : string -> constr_expr
+    -> syntax_modifier list -> scope_name option -> unit
+
+val add_syntax_extension : string -> syntax_modifier list -> unit
 
 val print_grammar : string -> string -> unit