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

16 files changed, 453 insertions, 356 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 9d00e63f4d..b2154c74d7 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -88,7 +88,7 @@ let rec explain_exn_default = function
       hov 0 (str "Error: Fail tactic always fails (level " ++ 
 	       int i ++ str").")
   | Stdpp.Exc_located (loc,exc) ->
-      hov 0 ((if loc = Ast.dummy_loc then (mt ())
+      hov 0 ((if loc = dummy_loc then (mt ())
                else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
                ++ explain_exn_default exc)
   | Lexer.Error Illegal_character -> 
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 2207608a87..1703a072da 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -10,11 +10,12 @@
 
 (*i*)
 open Pp
+open Util
 (*i*)
 
 (* Error report. *)
 
-val print_loc : Coqast.loc -> std_ppcmds
+val print_loc : loc -> std_ppcmds
 
 val explain_exn : exn -> std_ppcmds
 
diff --git a/toplevel/class.mli b/toplevel/class.mli
index 671219c3cb..8311be4a55 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -46,9 +46,9 @@ val try_add_new_coercion_with_source : global_reference -> strength ->
 val try_add_new_identity_coercion : identifier -> strength ->
   source:cl_typ -> target:cl_typ -> unit
 
-val add_coercion_hook : Proof_type.declaration_hook
+val add_coercion_hook : Tacexpr.declaration_hook
 
-val add_subclass_hook : Proof_type.declaration_hook
+val add_subclass_hook : Tacexpr.declaration_hook
 
 (* [try_add_new_class ref] declares [ref] as a new class; usually,
    this is done implicitely by [try_add_new_coercion]'s functions *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index e0f792a838..19842ea627 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -24,11 +24,10 @@ open Nametab
 open Names
 open Libnames
 open Nameops
-open Coqast
-open Ast
+open Topconstr
 open Library
 open Libobject
-open Astterm
+open Constrintern
 open Proof_type
 open Tacmach
 open Safe_typing
@@ -37,6 +36,7 @@ open Typeops
 open Indtypes
 open Vernacexpr
 open Decl_kinds
+open Pretyping
 
 let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
 let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
@@ -45,14 +45,14 @@ let rec abstract_rawconstr c = function
   | [] -> c
   | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_rawconstr c bl)
   | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> mkLambdaC(x,t,b)) idl
+      List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
         (abstract_rawconstr c bl)
 
 let rec prod_rawconstr c = function
   | [] -> c
   | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_rawconstr c bl)
   | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> mkProdC(x,t,b)) idl
+      List.fold_right (fun x b -> mkProdC([x],t,b)) idl
         (prod_rawconstr c bl)
 
 let rec destSubCast c = match kind_of_term c with
@@ -119,7 +119,8 @@ let declare_definition ident local bl red_option c typopt =
         declare_global_definition ident ce' local
 
 let syntax_definition ident c =
-  let c = interp_rawconstr Evd.empty (Global.env()) c in 
+  let c = 
+interp_aconstr c in 
   Syntax_def.declare_syntactic_definition ident c;
   if_verbose message ((string_of_id ident) ^ " is now a syntax macro")
 
@@ -236,7 +237,7 @@ let declare_mutual_with_eliminations mie =
   Indrec.declare_eliminations kn;
   kn
 
-let eq_la (id,ast) (id',ast') = id = id' & alpha_eq(ast,ast')
+let eq_la (id,ast) (id',ast') = id = id' & (* alpha_eq(ast,ast') *) (warning "check paramaters convertibility"; true)
 
 let extract_coe lc =
   List.fold_right
@@ -306,12 +307,14 @@ let collect_non_rec env =
   in 
   searchrec [] 
 
-let build_recursive lnameargsardef = 
-  let lrecnames = List.map (fun (f,_,_,_) -> f) lnameargsardef
+let build_recursive lnameargsardef =
+  let lrecnames = List.map (fun (f,_,_,_) -> f) lnameargsardef 
   and sigma = Evd.empty
   and env0 = Global.env()
-  and nv = Array.of_list (List.map (fun (_,la,_,_) -> (List.length la) -1)
-                            lnameargsardef) 
+  and nv = Array.of_list 
+    (List.map
+      (fun (_,la,_,_) -> List.length (List.flatten (List.map fst la)) - 1)
+        lnameargsardef)
   in
   let fs = States.freeze() in
   let (rec_sign,arityl) = 
@@ -455,9 +458,9 @@ let build_scheme lnamedepindsort =
 
 let rec generalize_rawconstr c = function
   | [] -> c
-  | LocalRawDef (id,b)::bl -> Ast.mkLetInC(id,b,generalize_rawconstr c bl)
+  | LocalRawDef (id,b)::bl -> mkLetInC(id,b,generalize_rawconstr c bl)
   | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> Ast.mkProdC(x,t,b)) idl
+      List.fold_right (fun x b -> mkProdC([x],t,b)) idl
         (generalize_rawconstr c bl)
 
 let rec binders_length = function
@@ -465,10 +468,12 @@ let rec binders_length = function
   | LocalRawDef _::bl -> 1 + binders_length bl
   | LocalRawAssum (idl,_)::bl -> List.length idl + binders_length bl
 
-let start_proof_com sopt kind (bl,t) hook =
-  let env = Global.env () in
+let start_proof id kind c hook =
   let sign = Global.named_context () in
   let sign = clear_proofs sign in
+  Pfedit.start_proof id kind sign c hook
+
+let start_proof_com sopt kind (bl,t) hook =
   let id = match sopt with
     | Some id ->
         (* We check existence here: it's a bit late at Qed time *)
@@ -479,9 +484,10 @@ let start_proof_com sopt kind (bl,t) hook =
 	next_ident_away (id_of_string "Unnamed_thm")
 	  (Pfedit.get_all_proof_names ())
   in
+  let env = Global.env () in
   let c = interp_type Evd.empty env (generalize_rawconstr t bl) in
   let _ = Typeops.infer_type env c in
-  Pfedit.start_proof id kind sign c hook
+  start_proof id kind c hook
 
 let apply_tac_not_declare id pft = function
   | None -> error "Type of Let missing"
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 9b3d996195..791c33d66a 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -17,7 +17,10 @@ open Declare
 open Library
 open Libnames
 open Nametab
+open Tacexpr
 open Vernacexpr
+open Rawterm
+open Topconstr
 open Decl_kinds
 (*i*)
 
@@ -27,31 +30,32 @@ open Decl_kinds
    defined object *)
 
 val declare_definition : identifier -> definition_kind ->
-  local_binder list -> Tacred.red_expr option -> Coqast.t -> Coqast.t option
-    -> global_reference
+  local_binder list -> Tacred.red_expr option -> constr_expr ->
+    constr_expr option -> global_reference
 
-val syntax_definition : identifier -> Coqast.t -> unit
+val syntax_definition : identifier -> constr_expr -> unit
 
 val declare_assumption : identifier -> assumption_kind -> 
-  local_binder list -> Coqast.t -> global_reference
+  local_binder list -> constr_expr -> global_reference
 
 val build_mutual : inductive_expr list -> bool -> unit
 
 val declare_mutual_with_eliminations :
   Entries.mutual_inductive_entry -> mutual_inductive
 
-val build_recursive :
-  (identifier * ((identifier * Coqast.t) list) * Coqast.t * Coqast.t) list 
-  -> unit
+val build_recursive : fixpoint_expr list -> unit
 
-val build_corecursive :  (identifier * Coqast.t * Coqast.t) list -> unit
+val build_corecursive : cofixpoint_expr list -> unit
 
-val build_scheme : (identifier * bool * qualid located * Coqast.t) list -> unit
+val build_scheme : (identifier * bool * reference * rawsort) list -> unit
 
-val generalize_rawconstr : Coqast.t -> local_binder list -> Coqast.t
+val generalize_rawconstr : constr_expr -> local_binder list -> constr_expr
+
+val start_proof : identifier -> goal_kind -> constr ->
+  declaration_hook -> unit
 
 val start_proof_com : identifier option -> goal_kind -> 
-  (local_binder list * Coqast.t) -> Proof_type.declaration_hook -> unit
+  (local_binder list * constr_expr) -> declaration_hook -> unit
 
 (*s [save_named b] saves the current completed proof under the name it
 was started; boolean [b] tells if the theorem is declared opaque; it
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 10d459dde5..14f9de51d7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -11,37 +11,86 @@
 open Pp
 open Util
 open Names
+open Topconstr
 open Coqast
 open Ast
+open Ppextend
 open Extend
 open Esyntax
 open Libobject
 open Library
 open Summary
-open Astterm
+open Constrintern
 open Vernacexpr
 open Pcoq
+open Rawterm
+open Libnames
 
 (*************************
  **** PRETTY-PRINTING ****
  *************************)
 
-let globalize_typed_ast t =
-  let sign = Global.named_context () in
-  match t with
-  | Ast.PureAstNode t -> Ast.PureAstNode (globalize_constr t)
-  | _ -> (* TODO *) t
-
 (* This updates default parsers for Grammar actions and Syntax *)
 (* patterns by inserting globalization *)
 (* Done here to get parsing/g_*.ml4 non dependent from kernel *)
-let _ = Pcoq.set_globalizer globalize_typed_ast
+let constr_to_ast a =
+  Termast.ast_of_rawconstr (interp_rawconstr Evd.empty (Global.env()) a)
 
 (* This installs default quotations parsers to escape the ast parser *)
 (* "constr" is used by default in quotations found in the ast parser *) 
-let constr_parser_with_glob = Pcoq.map_entry Astterm.globalize_constr Constr.constr
-
-let _ = define_quotation true "constr" constr_parser_with_glob
+let constr_parser_with_glob = Pcoq.map_entry constr_to_ast Constr.constr
+
+let _ = define_ast_quotation true "constr" constr_parser_with_glob
+
+let add_name r = function
+  | Anonymous -> ()
+  | Name id -> r := id :: !r
+
+let make_aconstr vars a =
+  let bound_vars = ref [] in
+  let bound_binders = ref [] in
+  let rec aux = function
+  | RVar (_,id) ->
+      if List.mem id vars then bound_vars := id::!bound_vars;
+      AVar id
+  | RApp (_,g,args) -> AApp (aux g, List.map aux args)
+  | RLambda (_,na,ty,c) -> add_name bound_binders na; ALambda (na,aux ty,aux c)
+  | RProd (_,na,ty,c) -> add_name bound_binders na; AProd (na,aux ty,aux c)
+  | RLetIn (_,na,b,c) -> add_name bound_binders na; ALetIn (na,aux b,aux c)
+  | ROrderedCase (_,b,tyopt,tm,bv) ->
+      AOldCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
+  | RCast (_,c,t) -> ACast (aux c,aux t)
+  | RSort (_,s) -> ASort s
+  | RHole (_,w) -> AHole w
+  | RRef (_,r) -> ARef r
+  | RMeta (_,n) -> AMeta n
+  | RDynamic _ | RRec _ | RCases _ | REvar _ ->
+      error "Fixpoints, cofixpoints, existential variables and pattern-matching  not \
+allowed in abbreviatable expressions"
+  in
+  let a = aux a in
+  let find_type x =
+    if List.mem x !bound_binders then (x,ETIdent) else
+    if List.mem x !bound_vars then (x,ETConstr) else
+      error ((string_of_id x)^" is unbound in the right-hand-side") in
+  let typs = List.map find_type vars in
+  (a, typs)
+
+let _ = set_ast_to_rawconstr
+  (fun etyps a ->
+    let vl = List.map fst etyps in 
+    let r =
+      for_grammar (interp_rawconstr_gen Evd.empty (Global.env()) [] false vl) a
+    in
+    let a, typs = make_aconstr vl r in
+(*
+    List.iter2
+      (fun (x,typ) (x',typ') ->
+	assert (x=x');
+	if typ = ETConstr & typ' = ETIdent then
+	  error "cannot use a constr parser to parse an ident") etyps typs;
+*)
+    a)
 
 (* Pretty-printer state summary *)
 let _ = 
@@ -75,9 +124,8 @@ let add_syntax_obj whatfor sel =
   Lib.add_anonymous_leaf (inPPSyntax (interp_syntax_entry whatfor sel))
 
 
-(************************
- ******* GRAMMAR ********
- ************************)
+(**********************************************************************)
+(* Grammar                                                            *)
 
 let _ = 
   declare_summary "GRAMMAR_LEXER"
@@ -112,21 +160,17 @@ let (inGrammar, outGrammar) =
        classify_function = (fun (_,o) -> Substitute o);
        export_function = (fun x -> Some x)}
 
-let gram_define_entry (u,_ as univ) ((ntl,nt),et,assoc,rl) =
-  let etyp = match et with None -> entry_type_from_name u | Some e -> e in
-  create_entry_if_new univ nt etyp;
-  let etyp = match etyp with 
-    | AstListType -> ETastl
-    | GenAstType Genarg.ConstrArgType -> ETast
-    | PureAstType -> ETast
-    | _ -> error "Cannot arbitrarily extend non ast entries" in
-  (nt, etyp, assoc, rl)
+open Genarg
+let gram_define_entry (u,_ as univ) (nt,et,assoc,rl) =
+  if u = "tactic" or u = "vernac" then error "tactic and vernac not supported";
+  create_entry_if_new univ nt (entry_type_of_constr_entry_type et);
+  (nt, et, assoc, rl)
 
 let add_grammar_obj univ l =
   let u = create_univ_if_new univ in
   let entryl = List.map (gram_define_entry u) l in
   let g = interp_grammar_command univ get_entry_type entryl in
-  Lib.add_anonymous_leaf (inGrammar (Egrammar.AstGrammar g))
+  Lib.add_anonymous_leaf (inGrammar (Egrammar.Grammar g))
 
 let add_tactic_grammar g = 
   Lib.add_anonymous_leaf (inGrammar (Egrammar.TacticGrammar g))
@@ -156,80 +200,41 @@ let split str =
   in
   loop 0 0
 
-
-(* A notation comes with a grammar rule, a pretty-printing rule, an
-   identifiying pattern called notation and an associated scope *)
-let load_infix _ (_,(gr,se,prec,ntn,scope,pat)) =
-  Symbols.declare_scope scope
-
-let open_infix i (_,(gr,se,prec,ntn,scope,pat)) =
-  if i=1 then begin
-    let b = Symbols.exists_notation_in_scope scope prec ntn pat in
-    (* Declare the printer rule and its interpretation *)
-    if not b then Esyntax.add_ppobject {sc_univ="constr";sc_entries=se};
-    (* Declare the grammar rule ... *)
-    if not (Symbols.exists_notation prec ntn) then Egrammar.extend_grammar gr;
-    (* ... and its interpretation *)
-    if not b then Symbols.declare_notation prec ntn pat scope
-  end
-
-let cache_infix o =
-  load_infix 1 o;
-  open_infix 1 o
-
-let subst_infix (_,subst,(gr,se,prec,ntn,scope,pat)) =
-  (Egrammar.subst_all_grammar_command subst gr,
-   list_smartmap (Extend.subst_syntax_entry Ast.subst_astpat subst) se,
-   prec,ntn,
-   scope,
-   Rawterm.subst_raw subst pat)
-
-let (inInfix, outInfix) =
-  declare_object {(default_object "INFIX") with
-       open_function = open_infix;
-       cache_function = cache_infix;
-       subst_function = subst_infix;
-       load_function = load_infix;
-       classify_function = (fun (_,o) -> Substitute o);
-       export_function = (fun x -> Some x)}
-
 (* Build the syntax and grammar rules *)
 
 type symbol =
   | Terminal of string
-  | NonTerminal of (int * parenRelation) * string
+  | NonTerminal of (int * parenRelation) * identifier
 
 let prec_assoc = function
   | Some(Gramext.RightA) -> (L,E)
   | Some(Gramext.LeftA) -> (E,L)
   | Some(Gramext.NonA) -> (L,L)
-  | None -> (E,L)  (* LEFTA by default *)
+  | None -> (L,L)   (* NONA by default *)
 
 let constr_tab =
   [| "constr0"; "constr1"; "constr2"; "constr3"; "lassoc_constr4";
-     "constr5"; "constr6"; "constr7"; "constr8"; "constr9"; "lconstr";
+     "constr5"; "constr6"; "constr7"; "constr"; "constr9"; "lconstr";
      "pattern" |]
 
 let level_rule (n,p) = if p = E then n else max (n-1) 0
 
 let constr_rule np = constr_tab.(level_rule np)
 
-let nonterm_meta nt var =
-  NonTerm(ProdPrimitive ("constr",nt), Some (var,ETast))
+let nonterm_meta nt var x =
+  match x with
+  | ETIdent -> NonTerm(ProdPrimitive ("constr","ident"), Some (var,x))
+  | ETConstr -> NonTerm(ProdPrimitive ("constr",nt), Some (var,x))
+  | ETReference -> NonTerm(ProdPrimitive ("constr","global"), Some (var,x))
 
+(* For old ast printer *)
 let meta_pattern m = Pmeta(m,Tany)
 
-let collect_metas sl =
-  List.fold_right
-    (fun it metatl -> match it with
-      | NonTerminal (_,m) -> Pcons(meta_pattern m, metatl)
-      | _ -> metatl)
-    sl Pnil
-
-let make_hunks symbols =
+(* For old ast printer *)
+let make_hunks_ast symbols =
   List.fold_right
     (fun it l -> match it with
-      | NonTerminal ((_,lp),m) -> PH (meta_pattern m, None, lp) :: l
+      | NonTerminal ((_,lp),m) -> PH (meta_pattern (string_of_id m), None, lp) :: l
       | Terminal s ->
 	  let n,s =
 	    if is_letter (s.[String.length s -1]) or is_letter (s.[0])
@@ -238,6 +243,32 @@ let make_hunks symbols =
 	  UNP_BRK (n, 1) :: RO s :: l)
     symbols []
 
+open Symbols
+
+type white_status = NextMaybeLetter | NextIsNotLetter | AddBrk of int
+
+let make_hunks symbols =
+  let (_,l) =
+  List.fold_right
+    (fun it (ws,l) -> match it with
+      | NonTerminal (prec,m) ->
+	  let u = UnpMetaVar (m,prec) in
+	  let l' = match ws with
+	    | AddBrk n -> UnpCut (PpBrk(n,1)) :: u :: l
+	    | _ -> u :: l in
+	  (NextMaybeLetter, l')
+      | Terminal s ->
+	  let n = if is_letter (s.[0]) then 1 else 0 in
+	  let s = 
+	    if (ws = NextMaybeLetter or ws = AddBrk 1)
+	      & is_letter (s.[String.length s -1])
+	    then s^" "
+	    else s
+	  in
+	  (AddBrk n, UnpTerminal s :: l))
+    symbols (NextMaybeLetter,[])
+  in l
+
 let string_of_prec (n,p) =
   (string_of_int n)^(match p with E -> "E" | L -> "L" | _ -> "")
 
@@ -246,7 +277,7 @@ let string_of_symbol = function
   | Terminal s -> s
 
 let assoc_of_symbol s l = match s with
-  | NonTerminal (lp,_) -> (level_rule lp,0,0) :: l
+  | NonTerminal (lp,_) -> level_rule lp :: l
   | Terminal _ -> l
 
 let string_of_assoc = function
@@ -255,30 +286,17 @@ let string_of_assoc = function
   | Some(Gramext.NonA) -> "NONA"
 
 let make_symbolic assoc n symbols =
-  ((n,0,0), List.fold_right assoc_of_symbol symbols []),
+  (n, List.fold_right assoc_of_symbol symbols []),
   (String.concat " " (List.map string_of_symbol symbols))
 
-let make_production =
+let make_production typs =
   List.map (function
-    | NonTerminal (lp,m) -> nonterm_meta (constr_rule lp) m
-    | Terminal s -> Term ("",s))
-
-let make_constr_grammar_rule n fname prod action =
-  Egrammar.AstGrammar
-  { gc_univ = "constr";
-    gc_entries =
-      [ { ge_name = constr_rule (n, E);
-          ge_type = ETast;
-          gl_assoc = None;
-          gl_rules =
-            [ { gr_name = fname;
-                gr_production = prod;
-                gr_action = action} ]
-        }
-      ]
-  }
+    | NonTerminal (lp,m) -> nonterm_meta (constr_rule lp) m (List.assoc m typs)
+    | Terminal s -> Term (Extend.terminal s))
 
+(*
 let create_meta n = "$e"^(string_of_int n)
+*)
 
 let strip s =
   let n = String.length s in
@@ -286,20 +304,18 @@ let strip s =
 
 let is_symbol s = not (is_letter s.[0])
 
-let rec find_symbols c_first c_next c_last vars new_var varprecl = function
+let rec find_symbols c_first c_next c_last vars varprecl = function
   | []    -> (vars, [])
   | x::sl when is_letter x.[0] ->
       let id = Names.id_of_string x in
-      if List.mem_assoc id vars then
-        error ("Variable "^x^" occurs more than once");
+      if List.mem id vars then error ("Variable "^x^" occurs more than once");
       let prec =
         try (List.assoc x varprecl,E)
         with Not_found ->
           if List.exists is_symbol sl then c_first else c_last in
       let (vars,l) =
-        find_symbols c_next c_next c_last vars (new_var+1) varprecl sl in
-      let meta = create_meta new_var in
-      ((id,ope ("META",[num new_var]))::vars, NonTerminal (prec, meta) :: l)
+        find_symbols c_next c_next c_last vars varprecl sl in
+      (id::vars, NonTerminal (prec,id) :: l)
 (*
   | "_"::sl ->
       warning "Found '_'";
@@ -310,18 +326,14 @@ let rec find_symbols c_first c_next c_last vars new_var varprecl = function
       (vars, NonTerminal (prec, meta) :: l)
 *)
   | s :: sl ->
-      let (vars,l) =
-        find_symbols c_next c_next c_last vars new_var varprecl sl in
+      let (vars,l) = find_symbols c_next c_next c_last vars varprecl sl in
       (vars, Terminal (strip s) :: l)
 
-let make_grammar_pattern symbols ntn =
-  Pnode("NOTATION",Pcons(Pquote (Str (dummy_loc,ntn)), collect_metas symbols))
-
-let make_grammar_rule n symbols ntn =
-  let prod = make_production symbols in
-  let action = Act (PureAstPat (make_grammar_pattern symbols ntn)) in
-  make_constr_grammar_rule n ("notation "^ntn) prod action
+let make_grammar_rule n typs symbols ntn =
+  let prod = make_production typs symbols in
+  ((if n=8 then "constr8" else constr_rule (n,E)),ntn,prod)
 
+(* For old ast printer *)
 let metas_of sl =
   List.fold_right
     (fun it metatl -> match it with
@@ -329,73 +341,162 @@ let metas_of sl =
       | _ -> metatl)
     sl []
 
+(* For old ast printer *)
 let make_pattern symbols ast =
-  let env = List.map (fun m -> (m,ETast)) (metas_of symbols) in
+  let env = List.map (fun m -> (string_of_id m,ETast)) (metas_of symbols) in
   fst (to_pat env ast)
 
+(* For old ast printer *)
 let make_syntax_rule n name symbols ast ntn sc =
   [{syn_id = name;
-    syn_prec = (n,0,0);
+    syn_prec = n;
     syn_astpat = make_pattern symbols ast;
-    syn_hunks = [UNP_SYMBOLIC(sc,ntn,UNP_BOX (PpHOVB 1, make_hunks symbols))]}]
-
-let subst_meta_ast subst a =
-  let found = ref [] in
-  let loc = dummy_loc in
-  let rec subst_rec subst = function
-  | Smetalam (_,s,body) -> Smetalam (loc,s,subst_rec subst body)
-  | Node(_,"META",_) -> error "Unexpected metavariable in notation"
-  | Node(_,"QUALID",[Nvar(_,id)]) as x ->
-      (try let a = List.assoc id subst in found:=id::!found; a
-       with Not_found -> x)
-  | Node(_,op,args) -> Node (loc,op, List.map (subst_rec subst) args)
-  | Slam(_,None,body) -> Slam(loc,None,subst_rec subst body)
-  | Slam(_,Some s,body) ->
-      (* Prévenir que "s" peut forcer une capturer à l'instantiation de la *)
-      (* règle de grammaire ?? *)
-      Slam(loc,Some s,subst_rec (List.remove_assoc s subst) body)
-  | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ as a -> set_loc loc a
-  | Dynamic _ as a -> (* Hum... what to do here *) a
-  in
-  let a = subst_rec subst a in
-  let l = List.filter (fun (x,_) -> not (List.mem x !found)) subst in
-  if l <> [] then
-    (let x = string_of_id (fst (List.hd l)) in
-     error (x^" is unbound in the right-hand-side"));
-  a
-
-let rec reify_meta_ast = function
-  | Smetalam (loc,s,body) -> Smetalam (loc,s,reify_meta_ast body)
-  | Node(loc,"META",[Num (_,n)]) -> Nmeta (loc,create_meta n)
+    syn_hunks = [UNP_SYMBOLIC(sc,ntn,UNP_BOX (PpHOVB 1, make_hunks_ast symbols))]}]
+
+let make_pp_rule symbols =
+  [UnpBox (PpHOVB 1, make_hunks symbols)]
+
+
+(**************************************************************************)
+(* Syntax extenstion: common parsing/printing rules and no interpretation *)
+
+let cache_syntax_extension (_,(prec,ntn,gr,se)) =
+  if not (Symbols.exists_notation prec ntn) then begin
+    Egrammar.extend_grammar (Egrammar.Notation gr);
+    Symbols.declare_printing_rule ntn (se,fst prec)
+  end
+
+let subst_notation_grammar subst x = x
+
+let subst_printing_rule subst x = x
+
+let subst_syntax_extension (_,subst,(prec,ntn,gr,se)) =
+  (prec,ntn,subst_notation_grammar subst gr,subst_printing_rule subst se)
+
+let (inSyntaxExtension, outSyntaxExtension) =
+  declare_object {(default_object "SYNTAX-EXTENSION") with
+       open_function = (fun i o -> if i=1 then cache_syntax_extension o);
+       cache_function = cache_syntax_extension;
+       subst_function = subst_syntax_extension;
+       classify_function = (fun (_,o) -> Substitute o);
+       export_function = (fun x -> Some x)}
+
+let interp_syntax_modifiers =
+  let rec interp assoc precl level etyps = function
+    | [] ->
+	let n = match level with None -> 1 | Some n -> n in
+	(assoc,precl,n,etyps)
+    | SetItemLevel (id,n) :: l ->
+	if List.mem_assoc id precl then error (id^"has already a precedence")
+	else interp assoc ((id,n)::precl) level etyps l
+    | SetLevel n :: l ->
+	if level <> None then error "already a level"
+	else interp assoc precl (Some n) etyps l
+    | SetAssoc a :: l ->
+	if assoc <> None then error "already an associativity"
+	else interp (Some a) precl level etyps l
+    | SetEntryType (s,typ) :: l ->
+	let id = id_of_string s in
+	if List.mem_assoc id etyps then error (s^"has already an entry type")
+	else interp assoc precl level ((id,typ)::etyps) l
+  in interp None [] None []
+
+let add_syntax_extension df modifiers =
+  let (assoc,varprecl,n,etyps) = interp_syntax_modifiers modifiers in
+  let (lp,rp) = prec_assoc assoc in
+  let (ids,symbs) = find_symbols (n,lp) (10,E) (n,rp) [] varprecl (split df) in
+  let (prec,notation) = make_symbolic assoc n symbs in
+  let gram_rule = make_grammar_rule n etyps symbs notation in
+  let pp_rule = make_pp_rule symbs in
+  Lib.add_anonymous_leaf (inSyntaxExtension(prec,notation,gram_rule,pp_rule))
+
+(**********************************************************************)
+(* Distfix, Infix, Notations *)
+
+(* A notation comes with a grammar rule, a pretty-printing rule, an
+   identifiying pattern called notation and an associated scope *)
+let load_infix _ (_,(gr,_,se,prec,ntn,scope,pat)) =
+  Symbols.declare_scope scope
+
+let open_infix i (_,(gr,oldse,se,prec,ntn,scope,pat)) =
+  if i=1 then begin
+    let b = Symbols.exists_notation_in_scope scope prec ntn pat in
+    (* Declare the printer rule and its interpretation *)
+    if not b then Esyntax.add_ppobject {sc_univ="constr";sc_entries=oldse};
+    (* Declare the grammar and printing rules ... *)
+    if not (Symbols.exists_notation prec ntn) then begin
+      Egrammar.extend_grammar (Egrammar.Notation gr);
+      Symbols.declare_printing_rule ntn (se,fst prec)
+    end;
+    (* ... and their interpretation *)
+    if not b then
+      Symbols.declare_notation ntn scope (pat,prec);
+  end
+
+let cache_infix o =
+  load_infix 1 o;
+  open_infix 1 o
+
+let subst_infix (_,subst,(gr,oldse,se,prec,ntn,scope,pat)) =
+  (subst_notation_grammar subst gr,
+   list_smartmap (Extend.subst_syntax_entry Ast.subst_astpat subst) oldse,
+   subst_printing_rule subst se,
+   prec,ntn,
+   scope,
+   subst_aconstr subst pat)
+
+let (inInfix, outInfix) =
+  declare_object {(default_object "INFIX") with
+       open_function = open_infix;
+       cache_function = cache_infix;
+       subst_function = subst_infix;
+       load_function = load_infix;
+       classify_function = (fun (_,o) -> Substitute o);
+       export_function = (fun x -> Some x)}
+
+(* For old ast printer *)
+let rec reify_meta_ast vars = function
+  | Smetalam (loc,s,body) -> Smetalam (loc,s,reify_meta_ast vars body)
+(*  | Node(loc,"META",[Num (_,n)]) -> Nmeta (loc,create_meta n)*)
   | Node(loc,"ISEVAR",[]) -> Nmeta (loc,"$_")
-  | Node(loc,op,args) -> Node (loc,op, List.map (reify_meta_ast) args)
-  | Slam(loc,na,body) -> Slam(loc,na,reify_meta_ast body)
+  | Node(loc,op,args) -> Node (loc,op, List.map (reify_meta_ast vars) args)
+  | Slam(loc,Some id,body) when List.mem id vars ->
+      Smetalam (loc,string_of_id id,reify_meta_ast vars body)
+  | Slam(loc,na,body) -> Slam(loc,na,reify_meta_ast vars body)
+  | Nvar (loc,id) when List.mem id vars -> Nmeta (loc,string_of_id id)
   | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ as a -> a
   | Dynamic _ as a -> (* Hum... what to do here *) a
 
-(* Distfix, Infix, Notations *)
+(* For old ast syntax *)
+let make_old_pp_rule n symbols r ntn scope vars =
+  let ast = Termast.ast_of_rawconstr r in
+  let ast = reify_meta_ast vars ast in
+  let rule_name = ntn^"_"^scope^"_notation" in
+  make_syntax_rule n rule_name symbols ast ntn scope
 
-let add_notation assoc n df ast varprecl sc =
+let add_notation df ast modifiers sc =
+  let (assoc,varprecl,n,_) = interp_syntax_modifiers modifiers in
   let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in
   let (lp,rp) = prec_assoc assoc in
-  let (subst,symbols) =
-    find_symbols (n,lp) (10,E) (n,rp) [] 1 varprecl (split df) in
+  let (vars,symbols) =
+    find_symbols (n,lp) (10,E) (n,rp) [] varprecl (split df) in
   let (prec,notation) = make_symbolic assoc n symbols in
-  let rule_name = notation^"_"^scope^"_notation" in
   (* To globalize... *)
-  let vars = List.map fst subst in
-  let ast = subst_meta_ast subst ast in
   let r = interp_rawconstr_gen Evd.empty (Global.env()) [] false vars ast in
-  let ast = Termast.ast_of_rawconstr r in
-  let ast = reify_meta_ast ast in
-  let gram_rule = make_grammar_rule n symbols notation in
-  let syntax_rule = make_syntax_rule n rule_name symbols ast notation scope in
-  Lib.add_anonymous_leaf
-    (inInfix(gram_rule,syntax_rule,prec,notation,scope,r))
+  let a,typs = make_aconstr vars r in
+  let typs =
+    List.map (fun (x,t) -> 
+      (x,if List.mem_assoc (string_of_id x) varprecl then ETConstr else t))
+      typs
+  in
+  let gram_rule = make_grammar_rule n typs symbols notation in
+  let pp_rule = make_pp_rule symbols in
+  let old_pp_rule = make_old_pp_rule n symbols r notation scope vars in
+  Lib.add_anonymous_leaf (inInfix(gram_rule,old_pp_rule,pp_rule,prec,notation,scope,a))
 
 (* TODO add boxes information in the expression *)
 
-let inject_var x = ope ("QUALID", [nvar (id_of_string x)])
+let inject_var x = CRef (Ident (dummy_loc, id_of_string x))
 
 (* To protect alphabetic tokens from being seen as variables *)
 let quote x = "\'"^x^"\'"
@@ -410,15 +511,16 @@ let rec rename x vars n = function
   | y::l ->
       let (vars,l) = rename x vars n l in (vars,(quote y)::l)
 
-let add_distfix assoc n df astf sc =
+let add_distfix assoc n df r sc =
   (* "x" cannot clash since ast is globalized (included section vars) *)
   let (vars,l) = rename "x" [] 1 (split df) in
   let df = String.concat " " l in
-  let ast = ope("APPLIST",astf::vars) in
-  add_notation assoc n df ast [] sc
+  let ast = mkAppC (mkRefC r, vars) in
+  let a = match assoc with None -> Gramext.LeftA | Some a -> a in
+  add_notation df ast [SetAssoc a;SetLevel n] sc
 
-let add_infix assoc n inf qid sc =
-  let pr = Astterm.globalize_qualid qid in
+let add_infix assoc n inf pr sc =
+(*  let pr = Astterm.globalize_qualid pr in*)
   (* check the precedence *)
   if n<1 or n>10 then
     errorlabstrm "Metasyntax.infix_grammar_entry"
@@ -428,9 +530,10 @@ let add_infix assoc n inf qid sc =
     errorlabstrm "Vernacentries.infix_grammar_entry"
       (str"Associativity Precedence must be 6,7,8 or 9.");
   *)
-  let metas = [inject_var "x"; inject_var "y"] in 
-  let ast = ope("APPLIST",pr::metas) in
-  add_notation assoc n ("x "^(quote inf)^" y") ast [] sc
+  let metas = [inject_var "x"; inject_var "y"] in
+  let ast = mkAppC (mkRefC pr,metas) in
+  let a = match assoc with None -> Gramext.LeftA | Some a -> a in
+  add_notation ("x "^(quote inf)^" y") ast [SetAssoc a;SetLevel n] sc
 
 (* Delimiters *)
 let load_delimiters _ (_,(_,_,scope,dlm)) =
@@ -438,9 +541,10 @@ let load_delimiters _ (_,(_,_,scope,dlm)) =
 
 let open_delimiters i (_,(gram_rule,pat_gram_rule,scope,dlm)) =
   if i=1 then begin
-    Egrammar.extend_grammar gram_rule;      (* For parsing terms *)
-    Egrammar.extend_grammar pat_gram_rule;  (* For parsing patterns *)
-    Symbols.declare_delimiters scope dlm    (* For printing *)
+    (* For parsing *)
+    Egrammar.extend_grammar (Egrammar.Delimiters (scope,gram_rule,pat_gram_rule));
+    (* For printing *)
+    Symbols.declare_delimiters scope dlm
   end
 
 let cache_delimiters o =
@@ -454,18 +558,13 @@ let (inDelim,outDelim) =
       load_function = load_delimiters;
       export_function = (fun x -> Some x) }
 
-let make_delimiter_rule (l,r as dlms) scope inlevel outlevel dlmname fname =
-  let symbols = [Terminal l; NonTerminal ((inlevel,E),"$e"); Terminal r] in
-  let prod = make_production symbols in
-  let args = Pcons(Pquote (string scope), Pcons (Pmeta ("$e",Tany), Pnil)) in
-  let action = Act (PureAstPat (Pnode(dlmname,args))) in
-  make_constr_grammar_rule outlevel fname prod action
+let make_delimiter_rule (l,r) inlevel =
+  let e = Nameops.make_ident "e" None in
+  let symbols = [Terminal l; NonTerminal ((inlevel,E),e); Terminal r] in
+  make_production [e,ETConstr] symbols
 
 let add_delimiters scope (l,r as dlms) =
   if l = "" or r = "" then error "Delimiters cannot be empty";
-  let fname = scope^"_delimiters" in
-  let gram_rule = make_delimiter_rule dlms scope 8 0 "DELIMITERS" fname in
-  let pfname = scope^"_patdelimiters" in
-  let pat_gram_rule = (* 11 is for "pattern" *)
-    make_delimiter_rule dlms scope 11 11 "PATTDELIMITERS" pfname in
+  let gram_rule = make_delimiter_rule dlms 0 (* constr0 *) in
+  let pat_gram_rule = make_delimiter_rule dlms 11 (* "pattern" *) in
   Lib.add_anonymous_leaf (inDelim(gram_rule,pat_gram_rule,scope,dlms))
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 1b667918ad..fbbe4a94e5 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
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 909cef6d08..7e0286b218 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -21,23 +21,17 @@ open Entries
 open Declare
 open Nametab
 open Coqast
-open Astterm
+open Constrintern
 open Command
 open Inductive
 open Safe_typing
 open Decl_kinds
 open Indtypes
 open Type_errors
+open Topconstr
 
 (********** definition d'un record (structure) **************)
 
-let occur_fields id fs =
-  List.exists
-    (function
-      | Vernacexpr.AssumExpr (_,a) -> Ast.occur_var_ast id a
-      | Vernacexpr.DefExpr (_,a,_) -> Ast.occur_var_ast id a)
-    fs
-
 let name_of id = if id = wildcard then Anonymous else Name id
 
 let interp_decl sigma env = function
@@ -45,7 +39,7 @@ let interp_decl sigma env = function
   | Vernacexpr.DefExpr(id,c,t) ->
       let c = match t with
 	| None -> c
-	| Some t -> Ast.ope("CAST",[c; t])
+	| Some t -> mkCastC (c,t)
       in
       let j = judgment_of_rawconstr Evd.empty env c in
       (Name id,Some j.uj_val, j.uj_type)
@@ -166,7 +160,7 @@ let declare_projections indsp coers fields =
 		let p = mkLambda (x, lift 1 rp, ccl') in
 		let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
 		let ci = Inductiveops.make_case_info env indsp
-		  (Some PrintLet) [| RegularPat |] in
+		  LetStyle [| RegularPat |] in
 		mkCase (ci, p, mkRel 1, [|branch|]) in
 	      let proj =
 	        it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 90b40020e9..ddee8f1d8f 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -13,6 +13,7 @@ open Names
 open Term
 open Sign
 open Vernacexpr
+open Topconstr
 (*i*)
 
 (* [declare_projections ref coers params fields] declare projections of
@@ -23,5 +24,5 @@ val declare_projections :
   inductive -> bool list -> rel_context -> constant option list
 
 val definition_structure :
-  identifier with_coercion * (identifier * Genarg.constr_ast) list *
+  identifier with_coercion * (identifier * constr_expr) list *
   (local_decl_expr with_coercion) list * identifier * sorts -> unit
diff --git a/toplevel/recordobj.mli b/toplevel/recordobj.mli
index 71dbc68165..2879e37d4f 100755
--- a/toplevel/recordobj.mli
+++ b/toplevel/recordobj.mli
@@ -9,4 +9,4 @@
 (* $Id$ *)
 
 val objdef_declare : Libnames.global_reference -> unit
-val add_object_hook : Proof_type.declaration_hook
+val add_object_hook : Tacexpr.declaration_hook
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 589bc9ad66..adc2328ab8 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -132,7 +132,7 @@ let print_highlight_location ib (bp,ep) =
 let print_location_in_file s fname (bp,ep) =
   let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl () ++
                    str"File " ++ str ("\""^fname^"\"")) in
-  if (bp,ep) = Ast.dummy_loc then 
+  if (bp,ep) = dummy_loc then 
     (errstrm ++ str", unknown location." ++ fnl ())
   else
     let ic = open_in fname in
@@ -158,7 +158,7 @@ let print_command_location ib dloc =
     | None -> (mt ())
 
 let valid_loc dloc (b,e) =
-  (b,e) <> Ast.dummy_loc
+  (b,e) <> dummy_loc
   & match dloc with
     | Some (bd,ed) -> bd<=b & e<=ed
     | _ -> true
@@ -208,7 +208,7 @@ let print_toplevel_error exc =
   let (dloc,exc) =
     match exc with
       | DuringCommandInterp (loc,ie) ->
-          if loc = Ast.dummy_loc then (None,ie) else (Some loc, ie)
+          if loc = dummy_loc then (None,ie) else (Some loc, ie)
       | _ -> (None, exc) 
   in
   let (locstrm,exc) =
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 937d05a223..4ad2c479ac 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -22,12 +22,12 @@ open Vernacinterp
    Use the module Coqtoplevel, which catches these exceptions
    (the exceptions are explained only at the toplevel). *)
 
-exception DuringCommandInterp of Coqast.loc * exn
+exception DuringCommandInterp of Util.loc * exn
 
 (* Like Exc_located, but specifies the outermost file read, the filename
    associated to the location of the error, and the error itself. *)
 
-exception Error_in_file of string * (string * Coqast.loc) * exn
+exception Error_in_file of string * (string * Util.loc) * exn
 
 (* Specifies which file is read. The intermediate file names are
    discarded here. The Drop exception becomes an error. We forget
@@ -37,13 +37,13 @@ let raise_with_file file exc =
   let (cmdloc,re) =
     match exc with
       | DuringCommandInterp(loc,e) -> (loc,e)
-      | e -> (Ast.dummy_loc,e) 
+      | e -> (dummy_loc,e) 
   in
   let (inner,inex) =
     match re with
-      | Error_in_file (_, (f,loc), e) when loc <> Ast.dummy_loc ->
+      | Error_in_file (_, (f,loc), e) when loc <> dummy_loc ->
           ((f, loc), e)
-      | Stdpp.Exc_located (loc, e) when loc <> Ast.dummy_loc ->
+      | Stdpp.Exc_located (loc, e) when loc <> dummy_loc ->
           ((file, loc), e)
       | _ -> ((file,cmdloc), re)
   in 
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index ad89461f25..5d53dab2af 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -13,18 +13,18 @@
 (* Like [Exc_located], but specifies the outermost file read, the input buffer
    associated to the location of the error, and the error itself. *)
 
-exception Error_in_file of string * (string * Coqast.loc) * exn
+exception Error_in_file of string * (string * Util.loc) * exn
 
 (* Read a vernac command on the specified input (parse only).
    Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
 
 val parse_phrase : Pcoq.Gram.parsable * in_channel option ->
-  Coqast.loc * Vernacexpr.vernac_expr
+  Util.loc * Vernacexpr.vernac_expr
 
 (* Reads and executes vernac commands from a stream.
    The boolean [just_parsing] disables interpretation of commands. *)
 
-exception DuringCommandInterp of Coqast.loc * exn
+exception DuringCommandInterp of Util.loc * exn
 exception End_of_input
 
 val just_parsing : bool ref
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3b899d8892..0506dd2da2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -20,17 +20,18 @@ open Term
 open Pfedit
 open Tacmach
 open Proof_trees
-open Astterm
+open Constrintern
 open Prettyp
 open Printer
 open Tacinterp
 open Command
 open Goptions
-(*open Declare*)
 open Libnames
 open Nametab
 open Vernacexpr
 open Decl_kinds
+open Topconstr
+open Pretyping
 
 (* Pcoq hooks *)
 
@@ -39,9 +40,9 @@ type pcoq_hook = {
   solve : int -> unit;
   abort : string -> unit;
   search : searchable -> dir_path list * bool -> unit;
-  print_name : qualid located -> unit;
+  print_name : reference -> unit;
   print_check : Environ.unsafe_judgment -> unit;
-  print_eval : (constr -> constr) -> Environ.env -> Coqast.t -> Environ.unsafe_judgment -> unit;
+  print_eval : (constr -> constr) -> Environ.env -> constr_expr -> Environ.unsafe_judgment -> unit;
   show_goal : int option -> unit
 }
 
@@ -175,14 +176,16 @@ let print_modules () =
   pr_vertical_list pr_dirpath only_loaded
 
 
-let print_module (loc,qid) =
+let print_module r =
+  let (loc,qid) = qualid_of_reference r in
   try
     let mp = Nametab.locate_module qid in
       msgnl (Printmod.print_module true mp)
   with
       Not_found -> msgnl (str"Unknown Module " ++ pr_qualid qid)
 
-let print_modtype (loc,qid) = 
+let print_modtype r = 
+  let (loc,qid) = qualid_of_reference r in
   try
     let kn = Nametab.locate_modtype qid in
       msgnl (Printmod.print_modtype kn)
@@ -211,7 +214,8 @@ let locate_file f =
     msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
 		  str"on loadpath"))
 
-let print_located_qualid (_,qid) =
+let print_located_qualid r =
+  let (loc,qid) = qualid_of_reference r in
   let msg = 
     try
       let ref = Nametab.locate qid in
@@ -274,7 +278,8 @@ let msg_notfound_library loc qid = function
 	(str"Unable to locate library" ++ spc () ++ pr_qualid qid))
   | e -> assert false
 
-let print_located_library (loc,qid) =
+let print_located_library r =
+  let (loc,qid) = qualid_of_reference r in
   try msg_found_library (Library.locate_qualified_library qid)
   with e -> msg_notfound_library loc qid e
 
@@ -286,6 +291,8 @@ let vernac_syntax = Metasyntax.add_syntax_obj
 
 let vernac_grammar = Metasyntax.add_grammar_obj
 
+let vernac_syntax_extension = Metasyntax.add_syntax_extension
+
 let vernac_delimiters = Metasyntax.add_delimiters
 
 let vernac_open_scope = Symbols.open_scope
@@ -293,20 +300,9 @@ let vernac_open_scope = Symbols.open_scope
 let vernac_arguments_scope qid scl =
   Symbols.declare_arguments_scope (global qid) scl
 
-let vernac_infix assoc n inf qid sc =
-  let sp = sp_of_global None (global qid) in
-  let dir = repr_dirpath (dirpath sp) in
-(*
-  if dir <> [] then begin
-    let modname = List.hd dir in
-    let long_inf = (string_of_id modname) ^ "." ^ inf in
-    Metasyntax.add_infix assoc n long_inf qid
-  end;
-*)
-  Metasyntax.add_infix assoc n inf qid sc
+let vernac_infix = Metasyntax.add_infix
 
-let vernac_distfix assoc n inf qid sc =
-  Metasyntax.add_distfix assoc n inf (Astterm.globalize_qualid qid) sc
+let vernac_distfix = Metasyntax.add_distfix
 
 let vernac_notation = Metasyntax.add_notation
 
@@ -392,15 +388,16 @@ let vernac_declare_module id binders_ast mty_ast_o mexpr_ast_o =
   match Lib.is_specification (), mty_ast_o, mexpr_ast_o with
     | _, None, None 
     | false, _, None ->
-	Declaremods.start_module Astmod.interp_modtype
+	Declaremods.start_module Modintern.interp_modtype
 	  id binders_ast mty_ast_o;
 	if_verbose message 
 	  ("Interactive Module "^ string_of_id id ^" started")
 	  
     | true, Some _, None
-    | true, _, Some (Coqast.Node(_,"QUALID",_))
+    | true, _, Some (CMEident _)
     | false, _, Some _ ->
-	Declaremods.declare_module Astmod.interp_modtype Astmod.interp_modexpr
+	Declaremods.declare_module 
+	  Modintern.interp_modtype Modintern.interp_modexpr
 	  id binders_ast mty_ast_o mexpr_ast_o;
 	if_verbose message 
 	  ("Module "^ string_of_id id ^" is defined")
@@ -422,12 +419,12 @@ let vernac_declare_module_type id binders_ast mty_ast_o =
   
   match mty_ast_o with
     | None ->
-	Declaremods.start_modtype Astmod.interp_modtype id binders_ast;
+	Declaremods.start_modtype Modintern.interp_modtype id binders_ast;
 	if_verbose message 
 	  ("Interactive Module Type "^ string_of_id id ^" started")
 	  
     | Some base_mty ->
-	Declaremods.declare_modtype Astmod.interp_modtype 
+	Declaremods.declare_modtype Modintern.interp_modtype 
 	  id binders_ast base_mty;
 	if_verbose message 
 	  ("Module Type "^ string_of_id id ^" is defined")
@@ -446,7 +443,7 @@ let vernac_record struc binders sort nameopt cfs =
   let const = match nameopt with 
     | None -> add_prefix "Build_" (snd struc)
     | Some id -> id in
-  let s = Astterm.interp_sort sort in
+  let s = interp_sort sort in
   Record.definition_structure (struc,binders,cfs,const,s)
 
   (* Sections *)
@@ -480,6 +477,7 @@ let is_obsolete_module (_,qid) =
   | _ -> false
 
 let vernac_require import _ qidl =
+  let qidl = List.map qualid_of_reference qidl in
   try
     match import with
       | None -> List.iter Library.read_library qidl
@@ -496,6 +494,7 @@ let vernac_require import _ qidl =
       raise e
       
 let vernac_import export qidl =
+  let qidl = List.map qualid_of_reference qidl in
   if export then
     List.iter Library.export_library qidl
   else
@@ -517,14 +516,14 @@ let vernac_canonical locqid =
 let cl_of_qualid = function
   | FunClass -> Classops.CL_FUN
   | SortClass -> Classops.CL_SORT
-  | RefClass (loc,qid) -> Class.class_of_ref (Nametab.global (loc, qid))
+  | RefClass r -> Class.class_of_ref (Nametab.global r)
 
-let vernac_coercion stre (loc,qid as locqid) qids qidt =
+let vernac_coercion stre ref qids qidt =
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
-  let ref = Nametab.global locqid in
-  Class.try_add_new_coercion_with_target ref stre source target;
-  if_verbose message ((string_of_qualid qid) ^ " is now a coercion")
+  let ref' = Nametab.global ref in
+  Class.try_add_new_coercion_with_target ref' stre source target;
+  if_verbose message ((string_of_reference ref) ^ " is now a coercion")
 
 let vernac_identity_coercion stre id qids qidt =
   let target = cl_of_qualid qidt in
@@ -619,8 +618,8 @@ let vernac_hints = Auto.add_hints
 let vernac_syntactic_definition id c = function
   | None -> syntax_definition id c
   | Some n ->
-      let l = list_tabulate (fun _ -> Ast.ope("ISEVAR",[])) n in
-      let c = Ast.ope ("APPLIST",c :: l) in
+      let l = list_tabulate (fun _ -> (CHole (dummy_loc),None)) n in
+      let c = CApp (dummy_loc,c,l) in
       syntax_definition id c
 
 let vernac_declare_implicits locqid = function
@@ -785,7 +784,8 @@ let vernac_print = function
   | PrintHintDbName s -> Auto.print_hint_db_by_name s
   | PrintHintDb -> Auto.print_searchtable ()
 
-let global_loaded_library (loc, qid) =
+let global_loaded_library r =
+  let (loc,qid) = qualid_of_reference r in
   try Nametab.locate_loaded_library qid
   with Not_found -> 
     user_err_loc (loc, "global_loaded_library",
@@ -834,7 +834,7 @@ let vernac_abort = function
       if !pcoq <> None then (out_some !pcoq).abort ""
   | Some id ->
       delete_proof id;
-      let s = string_of_id id in
+      let s = string_of_id (snd id) in
       if_verbose message ("Goal "^s^" aborted");
       if !pcoq <> None then (out_some !pcoq).abort s
 
@@ -1008,12 +1008,13 @@ let interp c = match c with
   | VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel
   | VernacTacticGrammar al -> Metasyntax.add_tactic_grammar al
   | VernacGrammar (univ,al) -> vernac_grammar univ al
+  | VernacSyntaxExtension (s,l) -> vernac_syntax_extension s l
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
   | VernacOpenScope sc -> vernac_open_scope sc
   | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl
   | VernacInfix (assoc,n,inf,qid,sc) -> vernac_infix assoc n inf qid sc
   | VernacDistfix (assoc,n,inf,qid,sc) -> vernac_distfix assoc n inf qid sc
-  | VernacNotation (assoc,n,inf,c,pl,sc) -> vernac_notation assoc n inf c pl sc
+  | VernacNotation (inf,c,pl,sc) -> vernac_notation inf c pl sc
 
   (* Gallina *)
   | VernacDefinition (k,id,d,f) -> vernac_definition k id d f
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 0eca1143f8..2e6e35df4f 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -13,6 +13,7 @@ open Names
 open Term
 open Vernacinterp
 open Vernacexpr
+open Topconstr
 (*i*)
 
 (* Vernacular entries. This module registers almost all the vernacular entries,
@@ -52,9 +53,9 @@ type pcoq_hook = {
   solve : int -> unit;
   abort : string -> unit;
   search : searchable -> dir_path list * bool -> unit;
-  print_name : Libnames.qualid Util.located -> unit;
+  print_name : Libnames.reference -> unit;
   print_check : Environ.unsafe_judgment -> unit;
-  print_eval : (constr -> constr) -> Environ.env -> Coqast.t -> Environ.unsafe_judgment -> unit;
+  print_eval : (constr -> constr) -> Environ.env -> constr_expr -> Environ.unsafe_judgment -> unit;
   show_goal : int option -> unit
 }
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 122c0b0b24..be0f4d6788 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -10,12 +10,12 @@
 
 open Util
 open Names
-open Coqast
 open Tacexpr
 open Extend
 open Genarg
-open Symbols
+open Topconstr
 open Decl_kinds
+open Ppextend
 
 (* Toplevel control exceptions *)
 exception ProtectedLoop
@@ -30,41 +30,41 @@ type def_kind = DEFINITION | LET | LOCAL | THEOREM | LETTOP | DECL | REMARK
 open Libnames
 open Nametab
 
-type class_rawexpr = FunClass | SortClass | RefClass of qualid located
+type class_rawexpr = FunClass | SortClass | RefClass of reference
   
 type printable =
   | PrintTables
   | PrintLocalContext
   | PrintFullContext
-  | PrintSectionContext of qualid located
+  | PrintSectionContext of reference
   | PrintInspect of int
   | PrintGrammar of string * string
   | PrintLoadPath
   | PrintModules
-  | PrintModule of qualid located
-  | PrintModuleType of qualid located
+  | PrintModule of reference
+  | PrintModuleType of reference
   | PrintMLLoadPath
   | PrintMLModules
-  | PrintName of qualid located
-  | PrintOpaqueName of qualid located
+  | PrintName of reference
+  | PrintOpaqueName of reference
   | PrintGraph
   | PrintClasses
   | PrintCoercions
   | PrintCoercionPaths of class_rawexpr * class_rawexpr
   | PrintUniverses of string option
-  | PrintHint of qualid located
+  | PrintHint of reference
   | PrintHintGoal
   | PrintHintDbName of string
   | PrintHintDb
 
 type searchable =
-  | SearchPattern of pattern_ast
-  | SearchRewrite of pattern_ast
-  | SearchHead of qualid located
+  | SearchPattern of pattern_expr
+  | SearchRewrite of pattern_expr
+  | SearchHead of reference
 
 type locatable =
-  | LocateTerm of qualid located
-  | LocateLibrary of qualid located
+  | LocateTerm of reference
+  | LocateLibrary of reference
   | LocateFile of string
 
 type goable =
@@ -87,22 +87,22 @@ type showable =
   | ExplainTree of int list
 
 type comment =
-  | CommentConstr of constr_ast
+  | CommentConstr of constr_expr
   | CommentString of string
   | CommentInt of int
 
-type raw_constr_ast = t
+type raw_constr_expr = constr_expr
 
 type hints =
-  | HintsResolve of (identifier option * constr_ast) list
-  | HintsImmediate of (identifier option * constr_ast) list
-  | HintsUnfold of (identifier option * qualid located) list
-  | HintsConstructors of identifier * qualid located
-  | HintsExtern of identifier * int * raw_constr_ast * raw_tactic_expr
+  | HintsResolve of (identifier option * constr_expr) list
+  | HintsImmediate of (identifier option * constr_expr) list
+  | HintsUnfold of (identifier option * reference) list
+  | HintsConstructors of identifier * reference
+  | HintsExtern of identifier * int * raw_constr_expr * raw_tactic_expr
 
 type search_restriction =
-  | SearchInside of qualid located list
-  | SearchOutside of qualid located list
+  | SearchInside of reference list
+  | SearchOutside of reference list
 
 type option_value =
   | StringValue of string
@@ -111,7 +111,7 @@ type option_value =
 
 type option_ref_value =
   | StringRefValue of string
-  | QualidRefValue of qualid located
+  | QualidRefValue of reference
 
 type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
@@ -122,36 +122,23 @@ type export_flag    = bool (* true = Export;        false = Import         *)
 type specif_flag    = bool (* true = Specification; false = Implementation *)
 type inductive_flag = bool (* true = Inductive;     false = CoInductive    *)
 
-type sort_expr = t
+type sort_expr = Rawterm.rawsort
 
-type simple_binder = identifier * constr_ast
+type simple_binder = identifier * constr_expr
 type 'a with_coercion = coercion_flag * 'a
 type constructor_expr = simple_binder with_coercion
 type inductive_expr =
-    identifier *  simple_binder list * constr_ast * constructor_expr list
-type fixpoint_expr =
-    identifier * simple_binder list * constr_ast * constr_ast
-type cofixpoint_expr =
-    identifier * constr_ast * constr_ast
-type local_binder =
-  | LocalRawDef of identifier * constr_ast
-  | LocalRawAssum of identifier list * constr_ast
+    identifier *  simple_binder list * constr_expr * constructor_expr list
 type definition_expr =
-  | ProveBody of local_binder list * constr_ast
-  | DefineBody of local_binder list * raw_red_expr option * constr_ast
-      * constr_ast option
+  | ProveBody of local_binder list * constr_expr
+  | DefineBody of local_binder list * raw_red_expr option * constr_expr
+      * constr_expr option
 
 type local_decl_expr =
-  | AssumExpr of identifier * constr_ast
-  | DefExpr of identifier * constr_ast * constr_ast option
+  | AssumExpr of identifier * constr_expr
+  | DefExpr of identifier * constr_expr * constr_expr option
 
-type precedence = int
-type grammar_entry_ast = 
-  (loc * string) * Ast.entry_type option * 
-    grammar_associativity * raw_grammar_rule list
-
-type module_ast = Coqast.t
-type module_binder = identifier list * module_ast
+type module_binder = identifier list * module_type_ast
 
 type vernac_expr =
   (* Control *)
@@ -161,35 +148,35 @@ type vernac_expr =
   | VernacVar of identifier
 
   (* Syntax *) 
-  | VernacGrammar of string * grammar_entry_ast list
+  | VernacGrammar of string * raw_grammar_entry list
   | VernacTacticGrammar of
       (string * (string * grammar_production list) * raw_tactic_expr) list
-  | VernacSyntax of string * syntax_entry_ast list
+  | VernacSyntax of string * raw_syntax_entry list
+  | VernacSyntaxExtension of string * syntax_modifier list
   | VernacOpenScope of scope_name
   | VernacDelimiters of scope_name * (string * string)
-  | VernacArgumentsScope of qualid located * scope_name option list
+  | VernacArgumentsScope of reference * scope_name option list
   | VernacInfix of
-      grammar_associativity * precedence * string * qualid located
-      * scope_name option
+      grammar_associativity * precedence * string * reference *
+      scope_name option
   | VernacDistfix of
-      grammar_associativity * precedence * string * qualid located
-      * scope_name option
+      grammar_associativity * precedence * string * reference *
+      scope_name option
   | VernacNotation of
-      grammar_associativity * precedence * string * constr_ast
-      * (string * precedence) list * scope_name option
+      string * constr_expr * syntax_modifier list * scope_name option
 
   (* Gallina *)
   | VernacDefinition of definition_kind * identifier * definition_expr *
-      Proof_type.declaration_hook
+      declaration_hook
   | VernacStartTheoremProof of theorem_kind * identifier *
-      (local_binder list * Coqast.t) * bool * Proof_type.declaration_hook
+      (local_binder list * constr_expr) * bool * declaration_hook
   | VernacEndProof of opacity_flag * (identifier * theorem_kind option) option
-  | VernacExactProof of constr_ast
+  | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * simple_binder with_coercion list
   | VernacInductive of inductive_flag * inductive_expr list
   | VernacFixpoint of fixpoint_expr list
   | VernacCoFixpoint of cofixpoint_expr list
-  | VernacScheme of (identifier * bool * qualid located * sort_expr) list
+  | VernacScheme of (identifier * bool * reference * sort_expr) list
 
   (* Gallina extensions *)
   | VernacRecord of identifier with_coercion * simple_binder list
@@ -197,22 +184,22 @@ type vernac_expr =
   | VernacBeginSection of identifier
   | VernacEndSegment of identifier
   | VernacRequire of
-      export_flag option * specif_flag option * qualid located list
-  | VernacImport of export_flag * qualid located list
-  | VernacCanonical of qualid located
-  | VernacCoercion of strength * qualid located * class_rawexpr * class_rawexpr
+      export_flag option * specif_flag option * reference list
+  | VernacImport of export_flag * reference list
+  | VernacCanonical of reference
+  | VernacCoercion of strength * reference * class_rawexpr * class_rawexpr
   | VernacIdentityCoercion of strength * identifier * 
       class_rawexpr * class_rawexpr
 
   (* Modules and Module Types *)
   | VernacDeclareModule of identifier * 
-      module_binder list * module_ast option * module_ast option
+      module_binder list * module_type_ast option * module_ast option
   | VernacDeclareModuleType of identifier * 
-      module_binder list * module_ast option
+      module_binder list * module_type_ast option
 
   (* Solving *)
   | VernacSolve of int * raw_tactic_expr
-  | VernacSolveExistential of int * constr_ast
+  | VernacSolveExistential of int * constr_expr
 
   (* Auxiliary file and library management *)
   | VernacRequireFrom of export_flag * specif_flag option * identifier * string
@@ -227,7 +214,7 @@ type vernac_expr =
   | VernacRestoreState of string
 
   (* Resetting *)
-  | VernacResetName of identifier
+  | VernacResetName of identifier located
   | VernacResetInitial
   | VernacBack of int
 
@@ -236,18 +223,18 @@ type vernac_expr =
       loc * (identifier located * raw_tactic_expr) list
   | VernacHints of string list * hints
   | VernacHintDestruct of
-      identifier * (bool,unit) location * constr_ast * int * raw_tactic_expr
-  | VernacSyntacticDefinition of identifier * constr_ast * int option
-  | VernacDeclareImplicits of qualid located * int list option
-  | VernacSetOpacity of opacity_flag * qualid located list
+      identifier * (bool,unit) location * constr_expr * int * raw_tactic_expr
+  | VernacSyntacticDefinition of identifier * constr_expr * int option
+  | VernacDeclareImplicits of reference * int list option
+  | VernacSetOpacity of opacity_flag * reference list
   | VernacUnsetOption of Goptions.option_name
   | VernacSetOption of Goptions.option_name * option_value
   | VernacAddOption of Goptions.option_name * option_ref_value list
   | VernacRemoveOption of Goptions.option_name * option_ref_value list
   | VernacMemOption of Goptions.option_name * option_ref_value list
   | VernacPrintOption of Goptions.option_name
-  | VernacCheckMayEval of raw_red_expr option * int option * constr_ast
-  | VernacGlobalCheck of constr_ast
+  | VernacCheckMayEval of raw_red_expr option * int option * constr_expr
+  | VernacGlobalCheck of constr_expr
   | VernacPrint of printable
   | VernacSearch of searchable * search_restriction
   | VernacLocate of locatable
@@ -255,12 +242,12 @@ type vernac_expr =
   | VernacNop
 
   (* Proof management *)
-  | VernacGoal of constr_ast
-  | VernacAbort of identifier option
+  | VernacGoal of constr_expr
+  | VernacAbort of identifier located option
   | VernacAbortAll
   | VernacRestart
   | VernacSuspend
-  | VernacResume of identifier option
+  | VernacResume of identifier located option
   | VernacUndo of int
   | VernacFocus of int option
   | VernacUnfocus