modules Ast et Pcoq

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

9 files changed, 1489 insertions, 2 deletions

diff --git a/parsing/ast.ml b/parsing/ast.ml
new file mode 100755
index 000000000..cb32a8b24
--- /dev/null
+++ b/parsing/ast.ml
@@ -0,0 +1,609 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Coqast
+open Pcoq
+
+let isMeta s = String.length s <> 0 & s.[0]='$'
+
+let dummy_loc = (0,0)
+
+let loc = function
+  | Node (loc,_,_) -> loc
+  | Nvar (loc,_) -> loc
+  | Slam (loc,_,_) -> loc
+  | Num (loc,_) -> loc
+  | Id (loc,_) -> loc
+  | Str (loc,_) -> loc
+  | Path (loc,_,_) -> loc
+  | Dynamic (loc,_) -> loc
+
+(* building a node with dummy location *)
+
+let ope(op,l) = Node(dummy_loc,op,l)
+let slam(idl,b) = Slam(dummy_loc,idl,b)
+let ide s = Id(dummy_loc,s)
+let nvar s = Nvar(dummy_loc,s)
+let num n = Num(dummy_loc,n)
+let str s = Str(dummy_loc,s)
+let path sl s = Path(dummy_loc,sl,s)
+let dynamic d = Dynamic(dummy_loc,d)
+
+let rec set_loc loc = function
+  | Node(_,op,al) -> Node(loc, op, List.map (set_loc loc) al)
+  | Slam(_,idl,b) -> Slam(loc,idl, set_loc loc b)
+  | Nvar(_,s) -> Nvar(loc,s)
+  | Id(_,s) -> Id(loc,s)
+  | Str(_,s) -> Str(loc,s)
+  | Num(_,s) -> Num(loc,s)
+  | Path(_,sl,s) -> Path(loc,sl,s)
+  | Dynamic(_,d) -> Dynamic(loc,d)
+
+(* raising located exceptions *)
+let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm))
+let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm))
+let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s)
+
+(* ast destructors *)
+let num_of_ast = function
+  | Num(_,n) -> n
+  | ast -> invalid_arg_loc (loc ast, "Ast.num_of_ast")
+
+let nvar_of_ast = function
+  | Nvar(_,s) -> s
+  | ast -> invalid_arg_loc (loc ast, "Ast.nvar_of_ast")
+
+let id_of_ast =  function
+  | Id(_,s) -> s
+  | ast -> invalid_arg_loc (loc ast, "Ast.nvar_of_ast")
+
+(* patterns of ast *)
+type pat =
+  | Pquote of t
+  | Pmeta of string * tok_kind
+  | Pnode of string * patlist
+  | Pslam of string option * pat
+  | Pmeta_slam of string * pat
+
+and patlist =
+  | Pcons of pat * patlist
+  | Plmeta of string
+  | Pnil
+
+and tok_kind = Tnum | Tid | Tstr | Tpath | Tvar | Tany | Tlist
+
+(* semantic actions of grammar rules *)
+type act =
+  | Aast of pat
+  | Aastlist of patlist
+  | Acase of act * (pat * act) list
+  | Acaselist of act * (patlist * act) list
+
+(* values associated to variables *)
+type v =
+  | Vast of t
+  | Vastlist of t list
+
+type env = (string * v) list
+
+(* Pretty-printing *)
+let rec print_ast ast =
+  match ast with
+    | Num(_,n) -> [< 'iNT n >]
+    | Str(_,s) -> [< 'qS s >]
+    | Path(_,sl,u) -> 
+	[< prlist (fun s -> [< 'sTR"#"; 'sTR s >]) sl; 'sTR"."; 'sTR u >]
+    | Id (_,s) -> [< 'sTR"{" ; 'sTR s ; 'sTR"}" >]
+    | Nvar(_,s) -> [< 'sTR s >]
+    | Node(_,op,l) ->
+        hOV 3 [< 'sTR"(" ; 'sTR op ; 'sPC ; print_astl l; 'sTR")" >]
+    | Slam(_,None,ast) -> hOV 1 [< 'sTR"[<>]"; print_ast ast >]
+    | Slam(_,Some x,ast) ->
+        hOV 1 [< 'sTR"["; 'sTR x; 'sTR"]"; 'cUT; print_ast ast >]
+    | Dynamic(_,d) ->
+	hOV 0 [< 'sTR"<dynamic: "; 'sTR(Dyn.tag d); 'sTR">" >]
+
+and print_astl astl =
+  prlist_with_sep pr_spc print_ast astl
+
+let print_ast_cast = function
+  | Tany -> [< >]
+  | Tvar -> [< 'sTR":var" >]
+  | Tid -> [< 'sTR":id" >]
+  | Tstr -> [< 'sTR":str" >]
+  | Tpath -> [< 'sTR":path" >]
+  | Tnum -> [< 'sTR":num" >]
+  | Tlist -> [< 'sTR":list" >]
+
+let rec print_astpat = function
+  | Pquote ast -> [< 'sTR"'"; print_ast ast >]
+  | Pmeta(s,tk) -> [< 'sTR s; print_ast_cast tk >]
+  | Pmeta_slam(s,b) ->
+      hOV 1 [< 'sTR"["; 'sTR s; 'sTR"]"; 'cUT; print_astpat b >]
+  | Pnode(op,al) ->
+      hOV 2 [< 'sTR"(" ; 'sTR op; 'sPC; print_astlpat al; 'sTR")" >]
+  | Pslam(None,b) -> hOV 1 [< 'sTR"[<>]"; 'cUT; print_astpat b >]
+  | Pslam(Some s,b) ->
+      hOV 1 [< 'sTR"["; 'sTR s; 'sTR"]"; 'cUT; print_astpat b >]
+
+and print_astlpat = function
+  | Pnil -> [< >]
+  | Pcons(h,Pnil) -> hOV 1 [< print_astpat h >]
+  | Pcons(h,t) -> hOV 1 [< print_astpat h; 'sPC; print_astlpat t >]
+  | Plmeta(s) -> [< 'sTR"| "; 'sTR s >]
+
+
+let print_val = function
+  | Vast a -> print_ast a
+  | Vastlist al -> 
+      hOV 1 [< 'sTR"["; prlist_with_sep pr_spc print_ast al; 'sTR"]" >]
+
+
+(* Ast values environments *)
+
+let grammar_type_error (loc,s) =
+  anomaly_loc (loc,s,[< 'sTR"grammar type error: "; 'sTR s >])
+
+
+(* Coercions enforced by the user *)
+let check_cast loc a k =
+  match (k,a) with
+    | (Tany, _) -> ()
+    | (Tid, Id _) -> ()
+    | (Tvar, Nvar _) -> ()
+    | (Tpath, Path _) -> ()
+    | (Tstr, Str _) -> ()
+    | (Tnum, Num _) -> ()
+    | (Tlist, _) -> grammar_type_error (loc,"Ast.cast_val")
+    | _ -> user_err_loc (loc,"Ast.cast_val",
+                         [< 'sTR"cast _"; print_ast_cast k; 'sTR"failed" >])
+
+let rec coerce_to_var v = function
+  | Nvar(_,id) -> id 
+  | ast -> user_err_loc
+        (loc ast,"Ast.coerce_to_var",
+         [< 'sTR"the variable "; 'sTR v;
+            'sTR" was bound to"; 'bRK(1,1); print_ast ast; 'sPC;
+            'sTR"instead of a (list of) variable(s)." >])
+
+let env_assoc_value loc v env =
+  try 
+    List.assoc v env
+  with Not_found -> 
+    anomaly_loc
+      (loc,"Ast.env_assoc_value",
+       [< 'sTR"metavariable "; 'sTR v; 'sTR" is unbound." >])
+
+let env_assoc_list sigma (loc,v) =
+  match env_assoc_value loc v sigma with
+    | Vastlist al -> al
+    | Vast a -> [a]
+
+let env_assoc sigma k (loc,v) =
+  match env_assoc_value loc v sigma with
+    | Vast a -> check_cast loc a k; a
+    | _ -> grammar_type_error (loc,"Ast.env_assoc: "^v^" is an ast list")
+
+let env_assoc_nvars sigma (dloc,v) =
+  match env_assoc_value dloc v sigma with
+    | Vastlist al -> List.map (coerce_to_var v) al
+    | Vast ast -> [coerce_to_var v ast]
+
+let build_lams dloc idl ast =
+  List.fold_right (fun id lam -> Slam(dloc,Some id,lam)) idl ast
+
+
+(* Substitution *)
+
+(* Locations in quoted ast are wrong (they refer to the right hand
+   side of a grammar rule). A default location dloc is used whenever
+   we create an ast constructor. Locations in the binding list are trusted. *)
+
+let rec pat_sub dloc sigma pat =
+  match pat with
+    | Pmeta(pv,c) -> env_assoc sigma c (dloc,pv) 
+    | Pmeta_slam(pv,p) ->
+        let idl = env_assoc_nvars sigma (dloc,pv) in
+        build_lams dloc idl (pat_sub dloc sigma p)
+    | Pquote a -> set_loc dloc a
+    | Pnode(op,pl) -> Node(dloc, op, patl_sub dloc sigma pl)
+    | Pslam(os,p) -> Slam(dloc, os, pat_sub dloc sigma p)
+	  
+and patl_sub dloc sigma pl =
+  match pl with
+    | Pnil -> 
+	[]
+    | Plmeta pv -> 
+	env_assoc_list sigma (dloc,pv)
+    | Pcons(Pmeta(pv,Tlist), ptl) ->
+        (env_assoc_list sigma (dloc,pv))@(patl_sub dloc sigma ptl)
+    | Pcons(p1,ptl) -> 
+	(pat_sub dloc sigma p1)::(patl_sub dloc sigma ptl)
+
+
+(* Converting and checking free meta-variables *)
+
+type entry_env = (string * entry_type) list
+
+let type_of_meta env loc pv =
+  try 
+    List.assoc pv env
+  with Not_found ->
+    user_err_loc (loc,"Ast.type_of_meta",
+                  [< 'sTR"variable "; 'sTR pv; 'sTR" is unbound" >])
+
+let check_ast_meta env loc pv =
+  if (type_of_meta env loc pv) <> ETast then
+    user_err_loc (loc,"Ast.check_ast_meta",
+                  [< 'sTR"variable "; 'sTR pv; 'sTR" is a List" >])
+
+let rec val_of_ast env ast =
+  match ast with
+    | Nvar(loc,pv) when isMeta pv ->
+        check_ast_meta env loc pv;
+        Pmeta(pv,Tany)
+    | Id(loc,pv) when isMeta pv ->
+        check_ast_meta env loc pv;
+        Pmeta(pv,Tid)
+    | Node(_,"$QUOTE",[qast]) -> Pquote (set_loc dummy_loc qast)
+    | Slam(loc,Some s,a) when isMeta s ->
+        let _ = type_of_meta env loc s in (* ids are coerced to id lists *)
+        Pmeta_slam(s, val_of_ast env a)
+    | (Path _|Num _|Id _|Str _|Nvar _) -> Pquote (set_loc dummy_loc ast)
+    | Slam(_,os,b) -> Pslam(os, val_of_ast env b)
+    | Node(loc,op,_) when isMeta op ->
+        user_err_loc(loc,"Ast.val_of_ast",
+                     [< 'sTR"no metavariable in operator position." >])
+    | Node(_,op,args) -> Pnode(op, vall_of_astl env args)
+    | Dynamic(loc,_) ->
+	invalid_arg_loc(loc,"val_of_ast: dynamic")
+	  
+and vall_of_astl env astl =
+  match astl with 
+    | (Node(loc,"$LIST",[Nvar(locv,pv)]))::asttl when isMeta pv ->
+        if type_of_meta env locv pv = ETastl then
+          if asttl = [] then 
+	    Plmeta pv
+          else 
+	    Pcons(Pmeta(pv,Tlist), vall_of_astl env asttl)
+        else 
+	  user_err_loc (loc,"Ast.vall_of_astl",
+                        [< 'sTR"variable "; 'sTR pv;
+                           'sTR" is not a List" >])
+    | ast::asttl -> 
+	Pcons (val_of_ast env ast, vall_of_astl env asttl)
+    | [] -> Pnil
+
+
+(* Alpha-conversion *)
+	  
+let rec alpha_var id1 id2 = function
+  | (i1,i2)::_ when i1=id1 -> i2 = id2
+  | (i1,i2)::_ when i2=id2 -> i1 = id1
+  | _::idl -> alpha_var id1 id2 idl
+  | [] -> id1 = id2
+
+let rec alpha alp a1 a2 =
+  match (a1,a2) with
+    | (Node(_,op1,tl1),Node(_,op2,tl2)) ->
+        (op1 = op2) & (List.length tl1 = List.length tl2)
+        & (List.for_all2 (alpha alp) tl1 tl2)
+    | (Nvar(_,id1),Nvar(_,id2)) -> alpha_var id1 id2 alp
+    | (Slam(_,None,body1),Slam(_,None,body2)) -> alpha alp body1 body2
+    | (Slam(_,Some s1,body1),Slam(_,Some s2,body2)) ->
+        alpha ((s1,s2)::alp) body1 body2
+    | (Id(_,s1),Id(_,s2)) -> s1=s2
+    | (Str(_,s1),Str(_,s2)) -> s1=s2
+    | (Num(_,n1),Num(_,n2)) -> n1=n2
+    | (Path(_,sl1,s1),Path(_,sl2,s2)) -> sl1=sl2 & s1=s2
+    | _ -> false
+
+let alpha_eq (a1,a2)= alpha [] a1 a2
+
+let alpha_eq_val = function
+  | (Vast a1, Vast a2) -> alpha_eq (a1,a2)
+  | (Vastlist al1, Vastlist al2) ->
+      (List.length al1 = List.length al2)
+      & List.for_all2 (fun x y -> alpha_eq (x,y)) al1 al2
+  | _ ->  false
+
+
+exception No_match of string
+
+let no_match_loc (loc,s) = Stdpp.raise_with_loc loc (No_match s)
+
+(* Binds value v to variable var. If var is already bound, checks if the
+   its value is alpha convertible with v. This allows non-linear patterns.
+
+   Important note: The Metavariable $_ is a special case; it cannot be
+   bound, which is like _ in the ML matching. *)
+
+let bind_env sigma var v =
+  if var = "$_" then 
+    sigma
+  else
+    try
+      let vvar = List.assoc var sigma in
+      if alpha_eq_val (v,vvar) then sigma
+      else raise (No_match "Ast.bind_env: values do not match")
+    with Not_found -> 
+      (var,v)::sigma
+
+let bind_env_ast sigma var ast =
+  try 
+    bind_env sigma var (Vast ast)
+  with e -> 
+    Stdpp.raise_with_loc (loc ast) e
+
+let alpha_define sigma loc ps s =
+  try 
+    let _ = List.assoc ps sigma in sigma
+  with Not_found ->
+    if ps = "$_" then sigma else (ps, Vast(Nvar(loc,s)))::sigma
+
+
+(* Match an ast with an ast pattern. Returns the new environnement. *)
+
+let rec amatch alp sigma spat ast =
+  match (spat,ast) with
+    | (Pquote a, _) ->
+        if alpha alp a ast then 
+	  sigma
+        else 
+	  no_match_loc (loc ast,"quote does not match")
+    | (Pmeta(pv,Tany), _) -> bind_env_ast sigma pv ast
+    | (Pmeta(pv,Tvar), Nvar _) -> bind_env_ast sigma pv ast
+    | (Pmeta(pv,Tid), Id _) -> bind_env_ast sigma pv ast
+    | (Pmeta(pv,Tnum), Num _) -> bind_env_ast sigma pv ast
+    | (Pmeta(pv,Tstr), Str _) -> bind_env_ast sigma pv ast
+    | (Pmeta(pv,Tpath), Path _) -> bind_env_ast sigma pv ast
+    | (Pmeta(pv,Tlist),_) -> grammar_type_error (loc ast,"Ast.amatch")
+    | (Pmeta_slam(pv,pb), Slam(loc, Some s, b)) ->
+        amatch alp (bind_env_ast sigma pv (Nvar(loc,s))) pb b
+    | (Pnode(nodp,argp), Node(loc,op,args)) when nodp = op ->
+        (try amatchl alp sigma argp args
+         with e -> Stdpp.raise_with_loc loc e)
+    | (Pslam(None,bp), Slam(_,None,b)) -> amatch alp sigma bp b
+    | (Pslam(Some ps,bp), Slam(_,Some s,b)) -> amatch ((ps,s)::alp) sigma bp b
+    | _ -> no_match_loc (loc ast, "Ast.amatch")
+
+and amatchl alp sigma spatl astl =
+  match (spatl,astl) with
+    | (Pnil, []) -> sigma
+    | (Pcons(pat,patl), ast::asttl) ->
+        amatchl alp (amatch alp sigma pat ast) patl asttl
+    | (Plmeta pv, _) -> bind_env sigma pv (Vastlist astl)
+    | _ -> raise (No_match "Ast.amatchl")
+
+let ast_match = amatch []
+let astl_match = amatchl []
+
+let first_match pat_of_fun env ast sl =
+  let rec aux = function
+    | [] -> None
+    | (h::t) ->
+        (try Some (h, ast_match env (pat_of_fun h) ast)
+         with (No_match _| Stdpp.Exc_located (_,No_match _)) -> aux t)
+  in 
+  aux sl
+
+let first_matchl patl_of_fun env astl sl =
+  let rec aux = function
+    | [] -> None
+    | (h::t) ->
+        (try Some (h, astl_match env (patl_of_fun h) astl)
+         with (No_match _| Stdpp.Exc_located (_,No_match _)) -> aux t)
+  in 
+  aux sl
+    
+let bind_patvar env loc v etyp =
+  try
+    if List.assoc v env = etyp then 
+      env
+    else 
+      user_err_loc
+	(loc,"Ast.bind_patvar",
+	 [< 'sTR"variable "; 'sTR v;
+            'sTR" is bound several times with different types" >])
+  with Not_found -> 
+    if v="$_" then env else (v,etyp)::env
+      
+let make_astvar env loc v cast =
+  let env' = bind_patvar env loc v ETast in
+  (Pmeta(v,cast), env')
+
+(* Note: no metavar in operator position. necessary ? *)
+(* TODO: $SLAM pour recuperer tous les Slam d'un coup dans une liste *)
+let rec pat_of_ast env ast =
+  match ast with
+    | Nvar(loc,pv) when isMeta pv -> make_astvar env loc pv Tany
+    | Id(loc,pv) when isMeta pv -> make_astvar env loc pv Tid
+    | Slam(loc,Some s,a) when isMeta s ->
+        let senv = bind_patvar env loc s ETast in
+        let (pa,env') = pat_of_ast senv a in
+        (Pmeta_slam(s, pa), env')
+    | Node(_,"$VAR",[Nvar(loc,pv)]) when isMeta pv ->
+        make_astvar env loc pv Tvar
+    | Node(_,"$ID",[Nvar(loc,pv)]) when isMeta pv ->
+        make_astvar env loc pv Tid
+    | Node(_,"$NUM",[Nvar(loc,pv)]) when isMeta pv ->
+        make_astvar env loc pv Tnum
+    | Node(_,"$STR",[Nvar(loc,pv)]) when isMeta pv ->
+        make_astvar env loc pv Tstr
+    | Node(_,"$PATH",[Nvar(loc,pv)]) when isMeta pv ->
+        make_astvar env loc pv Tpath
+    | Node(_,"$QUOTE",[qast]) -> (Pquote (set_loc dummy_loc qast), env)
+    | Slam(_,os,b) ->
+        let (pb,env') = pat_of_ast env b in
+        (Pslam(os,pb), env')
+    | Node(loc,op,_) when isMeta op ->
+        user_err_loc(loc,"Ast.pat_of_ast",
+                     [< 'sTR"no metavariable in operator position." >])
+    | Node(_,op,args) ->
+        let (pargs, env') = patl_of_astl env args in
+        (Pnode(op,pargs), env')
+    | (Path _|Num _|Id _|Str _|Nvar _) -> (Pquote (set_loc dummy_loc ast), env)
+    | Dynamic(loc,_) ->
+        invalid_arg_loc(loc,"pat_of_ast: dynamic")
+	  
+and patl_of_astl env astl =
+  match astl with
+    | [Node(_,"$LIST",[Nvar(loc,pv)])] when isMeta pv ->
+        let penv = bind_patvar env loc pv ETastl in
+        (Plmeta pv, penv)
+    | [] -> (Pnil,env)
+    | ast::asttl ->
+        let (p1,env1) = pat_of_ast env ast in
+        let (ptl,env2) = patl_of_astl env1 asttl in
+        (Pcons (p1,ptl), env2)
+	
+let to_pat env ast =
+  match ast with
+    | Node(_,"ASTPAT",[p]) -> pat_of_ast env p
+    | _ -> invalid_arg_loc (loc ast,"Ast.to_pat")
+
+
+(* Ast with cases and metavariables *)
+
+let print_sig = function
+  | [] -> [< >]
+  | sigma ->
+      [< 'sTR"with constraints :"; 'bRK(1,1);
+         v 0 (prlist_with_sep pr_spc
+                (fun (x,v) -> [< 'sTR x; 'sTR" = "; hOV 0 (print_val v) >])
+                sigma) >]
+
+let case_failed loc sigma e pats =
+  user_err_loc
+    (loc,"Ast.eval_act",
+     [< 'sTR"Grammar case failure. The ast"; 'sPC; print_ast e;
+        'sPC; 'sTR"does not match any of the patterns :";
+        'bRK(1,1); v 0 (prlist_with_sep pr_spc print_astpat pats); 'fNL;
+        print_sig sigma >])
+
+let caselist_failed loc sigma el pats =
+  user_err_loc
+    (loc,"Ast.eval_act",
+     [< 'sTR"Grammar case failure. The ast list"; 'bRK(1,1); print_astl el;
+        'sPC; 'sTR"does not match any of the patterns :";
+        'bRK(1,1); v 0 (prlist_with_sep pr_spc print_astlpat pats); 'fNL;
+        print_sig sigma >])
+
+let rec eval_act dloc sigma act =
+  match act with
+    | Aast pat -> Vast (pat_sub dloc sigma pat)
+    | Aastlist patl -> Vastlist (patl_sub dloc sigma patl)
+    | Acase(e,ml) ->
+        (match eval_act dloc sigma e with
+           | Vast esub ->
+               (match first_match fst sigma esub ml with
+                  | Some((_,a),sigma_pat) -> eval_act dloc sigma_pat a
+                  | _ -> case_failed dloc sigma esub (List.map fst ml))
+           | _ -> grammar_type_error (dloc,"Ast.eval_act"))
+    | Acaselist(e,ml) ->
+        (match eval_act dloc sigma e with
+           | Vastlist elsub ->
+               (match first_matchl fst sigma elsub ml with
+                  | Some((_,a),sigma_pat) -> eval_act dloc sigma_pat a
+                  | _ -> caselist_failed dloc sigma elsub (List.map fst ml))
+           | _ -> grammar_type_error (dloc,"Ast.eval_act"))
+
+(* TODO: case sur des variables uniquement -> pas de pb de conflit Ast/List *)
+let rec act_of_ast vars etyp ast =
+  match ast with
+    | Node(_,"$CASE",(a::et::cl)) ->
+        let atyp = entry_type et in
+        let pa = act_of_ast vars atyp a in
+        (match atyp with
+           | ETast ->
+               let acl = List.map (case vars etyp) cl in
+               Acase (pa,acl)
+           | ETastl ->
+               let acl = List.map (caselist vars etyp) cl in
+               Acaselist (pa,acl))
+    | Node(_,"ASTLIST",al) ->
+        (match (etyp,al) with
+           | (ETast,[a]) -> Aast (val_of_ast vars a)
+           | (ETastl,_) -> Aastlist (vall_of_astl vars al)
+           | (ETast,_) -> user_err_loc
+                 (loc ast,"Ast.act_of_ast",
+                  [< 'sTR
+                       "entry type is Ast, but the right hand side is a list"
+                  >]))
+    | _ -> invalid_arg_loc (loc ast,"Ast.act_of_ast: ill-formed")
+
+and case vars etyp ast =
+  match ast with
+    | Node(_,"CASE",[Node(loca,"ASTLIST",pl);a]) ->
+        (match pl with
+           | [p] ->
+               let (apl,penv) = pat_of_ast vars p in
+               let aa = act_of_ast penv etyp a in
+               (apl,aa)
+           | _ -> user_err_loc
+                 (loca,"Ast.case",
+                  [< 'sTR"case pattern for an ast should be a single ast" >]))
+    | _ -> invalid_arg_loc (loc ast,"Ast.case")
+	  
+and caselist vars etyp ast =
+  match ast with
+    | Node(_,"CASE",[Node(_,"ASTLIST",pl);a]) ->
+        let (apl,penv) = patl_of_astl vars pl in
+        let aa = act_of_ast penv etyp a in
+        (apl,aa)
+    | _ -> invalid_arg_loc (loc ast,"Ast.caselist")
+
+let to_act_check_vars env etyp ast =
+  match ast with
+    | Node(_,"ASTACT",[a]) -> act_of_ast env etyp a
+    | _ -> invalid_arg_loc (loc ast,"Ast.to_act_env")
+
+
+(* Hash-consing *)
+module Hloc = Hashcons.Make(
+  struct
+    type t = Coqast.loc
+    type u = unit
+    let equal (b1,e1) (b2,e2) = b1=b2 & e1=e2
+    let hash_sub () x = x
+    let hash = Hashtbl.hash
+  end)
+
+module Hast = Hashcons.Make(
+  struct
+    type t = Coqast.t
+    type u = (Coqast.t -> Coqast.t) * ((loc -> loc) * (string -> string))
+    let hash_sub (hast,(hloc,hstr)) = function
+      | Node(l,s,al) -> Node(hloc l, hstr s, List.map hast al)
+      | Nvar(l,s) -> Nvar(hloc l, hstr s)
+      | Slam(l,None,t) -> Slam(hloc l, None, hast t)
+      | Slam(l,Some s,t) -> Slam(hloc l, Some (hstr s), hast t)
+      | Num(l,n) -> Num(hloc l, n)
+      | Id(l,s) -> Id(hloc l, hstr s)
+      | Str(l,s) -> Str(hloc l, hstr s)
+      | Path(l,d,k) -> Path(hloc l, List.map hstr d, hstr k)
+      | Dynamic(l,d) -> Dynamic(hloc l, d)
+    let equal a1 a2 =
+      match (a1,a2) with
+        | (Node(l1,s1,al1), Node(l2,s2,al2)) ->
+            (l1==l2 & s1==s2 & List.length al1 = List.length al2)
+            & List.for_all2 (==) al1 al2
+        | (Nvar(l1,s1), Nvar(l2,s2)) -> l1==l2 & s1==s2
+        | (Slam(l1,None,t1), Slam(l2,None,t2)) -> l1==l2 & t1==t2
+        | (Slam(l1,Some s1,t1), Slam(l2,Some s2,t2)) -> l1==l2 & t1==t2
+        | (Num(l1,n1), Num(l2,n2)) -> l1==l2 & n1=n2
+        | (Id(l1,s1), Id(l2,s2)) -> l1==l2 & s1==s2
+        | (Str(l1,s1),Str(l2,s2)) -> l1==l2 & s1==s2
+        | (Path(l1,d1,k1), Path(l2,d2,k2)) ->
+            (l1==l2 & k1==k2 & List.length d1 = List.length d2)
+            & List.for_all2 (==) d1 d2
+        | _ -> false
+    let hash = Hashtbl.hash
+  end)
+
+let hcons_ast hstr =
+  let hloc = Hashcons.simple_hcons Hloc.f () in
+  let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr) in
+  (hast,hloc)
diff --git a/parsing/ast.mli b/parsing/ast.mli
new file mode 100755
index 000000000..67ab4b94a
--- /dev/null
+++ b/parsing/ast.mli
@@ -0,0 +1,107 @@
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+open Pcoq
+(*i*)
+
+(* Abstract syntax trees. *)
+
+(* raising located exceptions *)
+val anomaly_loc : Coqast.loc * string * std_ppcmds -> 'a
+val user_err_loc : Coqast.loc * string * std_ppcmds -> 'a
+val invalid_arg_loc : Coqast.loc * string -> 'a
+
+val dummy_loc : Coqast.loc
+val loc : Coqast.t -> Coqast.loc
+
+(* ast constructors with dummy location *)
+val ope : string * Coqast.t list -> Coqast.t
+val slam : string option * Coqast.t -> Coqast.t
+val nvar : string -> Coqast.t
+val ide : string -> Coqast.t
+val num : int -> Coqast.t
+val str : string -> Coqast.t
+val path : string list -> string -> Coqast.t
+val dynamic : Dyn.t -> Coqast.t
+
+val set_loc : Coqast.loc -> Coqast.t -> Coqast.t
+
+(* ast destructors *)
+val num_of_ast : Coqast.t -> int
+val id_of_ast : Coqast.t -> string
+val nvar_of_ast : Coqast.t -> string
+
+(* ast processing datatypes *)
+
+(* patterns of ast *)
+type pat =
+  | Pquote of Coqast.t
+  | Pmeta of string * tok_kind
+  | Pnode of string * patlist
+  | Pslam of string option * pat
+  | Pmeta_slam of string * pat
+
+and patlist =
+  | Pcons of pat * patlist
+  | Plmeta of string
+  | Pnil
+
+and tok_kind = Tnum | Tid | Tstr | Tpath | Tvar | Tany | Tlist
+
+(* semantic actions of grammar rules *)
+type act =
+  | Aast of pat
+  | Aastlist of patlist
+  | Acase of act * (pat * act) list
+  | Acaselist of act * (patlist * act) list
+
+(* values associated to variables *)
+type v =
+  | Vast of Coqast.t
+  | Vastlist of Coqast.t list
+
+type env = (string * v) list
+
+val coerce_to_var : string -> Coqast.t -> string
+
+exception No_match of string
+
+val isMeta : string -> bool
+
+val print_ast : Coqast.t -> std_ppcmds
+val print_astl : Coqast.t list -> std_ppcmds
+val print_astpat : pat -> std_ppcmds
+val print_astlpat : patlist -> std_ppcmds
+
+(* Meta-syntax operations: matching and substitution *)
+
+type entry_env = (string * entry_type) list
+
+val grammar_type_error : Coqast.loc * string -> 'a
+ 
+(* Converting and checking free meta-variables *)
+val pat_sub : Coqast.loc -> env -> pat -> Coqast.t
+val val_of_ast : entry_env -> Coqast.t -> pat
+val vall_of_astl : entry_env -> Coqast.t list -> patlist
+
+val alpha_eq : Coqast.t * Coqast.t -> bool
+val alpha_eq_val : v * v -> bool
+val bind_env : env -> string -> v -> env
+val ast_match : env -> pat -> Coqast.t -> env
+val astl_match : env -> patlist -> Coqast.t list -> env
+val first_match : ('a -> pat) -> env -> Coqast.t -> 'a list ->
+  ('a * env) option
+val first_matchl : ('a -> patlist) -> env -> Coqast.t list -> 'a list ->
+  ('a * env) option
+
+val to_pat : entry_env -> Coqast.t -> (pat * entry_env)
+
+val eval_act : Coqast.loc -> env -> act -> v
+val to_act_check_vars : entry_env -> entry_type -> Coqast.t -> act
+
+(* Hash-consing *)
+val hcons_ast: (string -> string) ->
+  (Coqast.t -> Coqast.t) * (Coqast.loc -> Coqast.loc)
+
diff --git a/parsing/coqast.ml b/parsing/coqast.ml
new file mode 100644
index 000000000..b0a825326
--- /dev/null
+++ b/parsing/coqast.ml
@@ -0,0 +1,65 @@
+
+(* $Id$ *)
+
+type loc = int * int
+
+type t =
+  | Node of loc * string * t list
+  | Nvar of loc * string
+  | Slam of loc * string option * t
+  | Num of loc * int
+  | Id of loc * string
+  | Str of loc * string
+  | Path of loc * string list* string
+  | Dynamic of loc * Dyn.t
+
+type the_coq_ast = t
+
+(* Hash-consing *)
+module Hloc = Hashcons.Make(
+  struct
+    type t = loc
+    type u = unit
+    let equal (b1,e1) (b2,e2) = b1=b2 & e1=e2
+    let hash_sub () x = x
+    let hash = Hashtbl.hash
+  end)
+
+module Hast = Hashcons.Make(
+  struct
+    type t = the_coq_ast
+    type u = (the_coq_ast -> the_coq_ast) * ((loc -> loc) * (string -> string))
+    let hash_sub (hast,(hloc,hstr)) = function
+      | Node(l,s,al) -> Node(hloc l, hstr s, List.map hast al)
+      | Nvar(l,s) -> Nvar(hloc l, hstr s)
+      | Slam(l,None,t) -> Slam(hloc l, None, hast t)
+      | Slam(l,Some s,t) -> Slam(hloc l, Some (hstr s), hast t)
+      | Num(l,n) -> Num(hloc l, n)
+      | Id(l,s) -> Id(hloc l, hstr s)
+      | Str(l,s) -> Str(hloc l, hstr s)
+      | Path(l,d,k) -> Path(hloc l, List.map hstr d, hstr k)
+      | Dynamic(l,d) -> Dynamic(hloc l, d)
+    let equal a1 a2 =
+      match (a1,a2) with
+        | (Node(l1,s1,al1), Node(l2,s2,al2)) ->
+            (l1==l2 & s1==s2 & List.length al1 = List.length al2)
+            & List.for_all2 (==) al1 al2
+        | (Nvar(l1,s1), Nvar(l2,s2)) -> l1==l2 & s1==s2
+        | (Slam(l1,None,t1), Slam(l2,None,t2)) -> l1==l2 & t1==t2
+        | (Slam(l1,Some s1,t1), Slam(l2,Some s2,t2)) -> l1==l2 & t1==t2
+        | (Num(l1,n1), Num(l2,n2)) -> l1==l2 & n1=n2
+        | (Id(l1,s1), Id(l2,s2)) -> l1==l2 & s1==s2
+        | (Str(l1,s1),Str(l2,s2)) -> l1==l2 & s1==s2
+        | (Path(l1,d1,k1), Path(l2,d2,k2)) ->
+            (l1==l2 & k1==k2 & List.length d1 = List.length d2)
+            & List.for_all2 (==) d1 d2
+        | _ -> false
+    let hash = Hashtbl.hash
+  end)
+
+let hcons_ast hstr =
+  let hloc = Hashcons.simple_hcons Hloc.f () in
+  let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr) in
+  (hast,hloc)
+
+
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
new file mode 100644
index 000000000..006b98b3e
--- /dev/null
+++ b/parsing/coqast.mli
@@ -0,0 +1,17 @@
+
+(* $Id$ *)
+
+type loc = int * int
+
+type t =
+  | Node of loc * string * t list
+  | Nvar of loc * string
+  | Slam of loc * string option * t
+  | Num of loc * int
+  | Id of loc * string
+  | Str of loc * string
+  | Path of loc * string list* string
+  | Dynamic of loc * Dyn.t
+
+val hcons_ast: (string -> string) -> (t -> t) * (loc -> loc)
+
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index b45b480dc..1e5b610c6 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -158,8 +158,7 @@ let rec pp bv = function
   | DOPN (AppL, [|c|]) ->
       pp bv c
   | DOPN (AppL, v) ->
-      [< 'sTR"("; prvect_with_sep (fun () -> [< 'sPC >]) (pp bv) v;
-	 'sTR")" >]
+      [< 'sTR"("; prvect_with_sep (fun () -> [< 'sPC >]) (pp bv) v; 'sTR")" >]
   | DOPN (Const sp, _) ->
       [< 'sTR"Const "; print_id (basename sp) >]
   | DOPN (MutInd (sp,i), _) ->
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 0c8f7f5f9..cbc4bc49e 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -5,6 +5,8 @@ val add_keyword : string -> unit
 
 val func : char Stream.t -> (string * string) Stream.t * (int -> int * int)
 
+val add_token : Token.pattern -> unit
+
 val tparse : string * string -> (string * string) Stream.t -> string
 
 val token_text : string * string -> string
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index 9a417622b..5a2f980f5 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -176,6 +176,10 @@ let func cs =
   in
   let ts = Stream.from next_token in
   (ts, find_loc loct)
+
+let add_token = function
+  | ("",kw) -> add_keyword kw
+  | _ -> ()
 	 
 let token_text = function
   | ("", t) -> "'" ^ t ^ "'"
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
new file mode 100644
index 000000000..714f29aea
--- /dev/null
+++ b/parsing/pcoq.ml4
@@ -0,0 +1,456 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+
+(* The lexer of Coq *)
+
+(* Note: removing a token.
+   We do nothing because remove_token is called only when removing a grammar
+   rule with Grammar.delete_rule. The latter command is called only when
+   unfreezing the state of the grammar entries (see GRAMMAR summary, file
+   env/metasyntax.ml). Therefore, instead of removing tokens one by one,
+   we unfreeze the state of the lexer. This restores the behaviour of the
+   lexer. B.B. *)
+
+let lexer = {
+  Token.func = Lexer.func;
+  Token.using = Lexer.add_token;
+  Token.removing = (fun _ -> ());
+  Token.tparse = Lexer.tparse;
+  Token.text = Lexer.token_text }
+
+module L =
+  struct
+    let lexer = lexer
+  end
+
+
+(* The parser of Coq *)
+module G = Grammar.Make(L)
+
+let grammar_delete e rls =
+  List.iter
+    (fun (_,_,lev) ->
+       List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
+    (List.rev rls)
+
+type typed_entry =
+  | Ast of Coqast.t G.Entry.e
+  | ListAst of Coqast.t list G.Entry.e
+
+
+type ext_kind =
+  | ByGrammar of
+      typed_entry * Gramext.position option *
+      (string option * Gramext.g_assoc option *
+       (Gramext.g_symbol list * Gramext.g_action) list) list
+  | ByGEXTEND of (unit -> unit) * (unit -> unit)
+
+
+let camlp4_state = ref []
+
+(* The apparent parser of Coq; encapsulate G to keep track of the
+   extensions. *)
+module Gram =
+  struct
+    type parsable = G.parsable
+    let parsable = G.parsable
+    let tokens = G.tokens
+    module Entry = G.Entry
+    module Unsafe = G.Unsafe
+
+    let extend e pos rls =
+      camlp4_state :=
+      (ByGEXTEND ((fun () -> grammar_delete e rls),
+                  (fun () -> G.extend e pos rls)))
+      :: !camlp4_state;
+      G.extend e pos rls
+    let delete_rule e pil =
+      errorlabstrm "Pcoq.delete_rule"
+        [< 'sTR "GDELETE_RULE forbidden." >]
+  end
+
+
+(* This extension command is used by the Grammar command *)
+let grammar_extend te pos rls =
+  camlp4_state := ByGrammar (te,pos,rls) :: !camlp4_state;
+  match te with
+      Ast e ->  G.extend e pos rls
+    | ListAst e -> G.extend e pos rls
+
+(* n is the number of extended entries (not the number of Grammar commands!)
+   to remove. *)
+let rec remove_grammars n =
+  if n>0 then
+    (match !camlp4_state with
+         [] -> anomaly "Pcoq.remove_grammars: too many rules to remove"
+       | ByGrammar(Ast e,_,rls)::t ->
+           grammar_delete e rls;
+           camlp4_state := t;
+           remove_grammars (n-1)
+       | ByGrammar(ListAst e,_,rls)::t ->
+           grammar_delete e rls;
+           camlp4_state := t;
+           remove_grammars (n-1)
+       | ByGEXTEND (undo,redo)::t ->
+           undo();
+           camlp4_state := t;
+           remove_grammars n;
+           redo();
+           camlp4_state := ByGEXTEND (undo,redo) :: !camlp4_state)
+
+
+
+(* An entry that checks we reached the end of the input. *)
+let eoi_entry en =
+  let e = Gram.Entry.create ((Gram.Entry.name en) ^ "_eoi") in
+  GEXTEND Gram
+    e: [ [ x = en; EOI -> x ] ]
+    ;
+  END;
+  e
+
+let map_entry f en =
+  let e = Gram.Entry.create ((Gram.Entry.name en) ^ "_map") in
+  GEXTEND Gram
+    e: [ [ x = en -> f x ] ]
+    ;
+  END;
+  e
+
+
+(* Parse a string, does NOT check if the entire string was read
+   (use eoi_entry) *)
+let parse_string f x =
+  let strm = Stream.of_string x in Gram.Entry.parse f (Gram.parsable strm)
+
+
+
+let slam_ast loc id ast =
+  match id with
+    Coqast.Nvar (_, s) -> Coqast.Slam (loc, Some s, ast)
+  | _ -> invalid_arg "Ast.slam_ast"
+
+
+type entry_type = ETast | ETastl
+
+let entry_type ast =
+  match ast with
+    Coqast.Id (_, "LIST") -> ETastl
+  | Coqast.Id (_, "AST") -> ETast
+  | _ -> invalid_arg "Ast.entry_type"
+
+
+let type_of_entry e =
+  match e with
+    Ast _ -> ETast
+  | ListAst _ -> ETastl
+
+
+type gram_universe = (string, typed_entry) Hashtbl.t
+
+
+let trace = ref false
+
+(*
+trace.val := True;
+*)
+
+(* The univ_tab is not part of the state. It contains all the grammar that
+   exist or have existed before in the session. *)
+let univ_tab = Hashtbl.create 7
+let get_univ s =
+  try Hashtbl.find univ_tab s with
+    Not_found ->
+      if !trace then
+        begin Printf.eprintf "[Creating univ %s]\n" s; flush stderr; () end;
+      let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u
+
+
+let get_entry (u, utab) s =
+  try Hashtbl.find utab s with
+    Not_found -> errorlabstrm "Pcoq.get_entry"
+        [< 'sTR"unknown grammar entry "; 'sTR u; 'sTR":"; 'sTR s >]
+
+
+let new_entry etyp (u, utab) s =
+  let ename = u ^ ":" ^ s in
+  let e =
+    match etyp with
+      ETast -> Ast (Gram.Entry.create ename)
+    | ETastl -> ListAst (Gram.Entry.create ename)
+  in
+  Hashtbl.add utab s e; e
+
+
+let create_entry (u, utab) s etyp =
+  try
+    let e = Hashtbl.find utab s in
+    if type_of_entry e <> etyp then
+      failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type")
+    else e
+  with
+    Not_found ->
+      if !trace then
+        begin
+          Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr; ()
+        end;
+      new_entry etyp (u, utab) s
+
+
+let force_entry_type (u, utab) s etyp =
+  try
+    let entry = Hashtbl.find utab s in
+    let extyp = type_of_entry entry in
+    if etyp = extyp then entry
+    else
+      begin
+        prerr_endline
+          ("Grammar entry " ^ u ^ ":" ^ s ^
+             " redefined with another type;\n older entry hidden.");
+        Hashtbl.remove utab s;
+        new_entry etyp (u, utab) s
+      end
+  with
+    Not_found -> new_entry etyp (u, utab) s
+
+
+
+
+
+(* Grammar entries *)
+
+module Command =
+  struct
+    let ucommand = snd (get_univ "command")
+    let gec s =
+      let e = Gram.Entry.create ("Command." ^ s) in
+      Hashtbl.add ucommand s (Ast e); e
+    
+    let gec_list s =
+      let e = Gram.Entry.create ("Command." ^ s) in
+      Hashtbl.add ucommand s (ListAst e); e
+
+    let abstraction_tail = gec "abstraction_tail"
+    let binder = gec "binder"
+    let cofixbinder = gec "cofixbinder"
+    let cofixbinders = gec_list "cofixbinders"
+    let command = gec "command"
+    let command0 = gec "command0"
+    let command1 = gec "command1"
+    let command10 = gec "command10"
+    let command2 = gec "command2"
+    let command3 = gec "command3"
+    let command5 = gec "command5"
+    let command6 = gec "command6"
+    let command7 = gec "command7"
+    let command8 = gec "command8"
+    let command9 = gec "command9"
+    let command91 = gec "command91"
+    let command_eoi = eoi_entry command
+    let equation = gec "equation"
+    let fixbinder = gec "fixbinder"
+    let fixbinders = gec_list "fixbinders"
+    let ident = gec "ident"
+    let lassoc_command4 = gec "lassoc_command4"
+    let lcommand = gec "lcommand"
+    let lsimple_pattern = Gram.Entry.create "Command.lsimple_pattern"
+    let ne_binder_list = gec_list "ne_binder_list"
+    let ne_command91_list = gec_list "ne_command91_list"
+    let ne_command9_list = gec_list "ne_command9_list"
+    let ne_command_list = gec_list "ne_command_list"
+    let ne_eqn_list = gec_list "ne_eqn_list"
+    let ne_ident_comma_list = gec_list "ne_ident_comma_list"
+    let ne_pattern_list = Gram.Entry.create "Command.ne_pattern_list"
+    let pattern = Gram.Entry.create "Command.pattern"
+    let pattern_list = Gram.Entry.create "Command.pattern_list"
+    let product_tail = gec "product_tail"
+    let raw_command = gec "raw_command"
+    let simple_pattern = Gram.Entry.create "Command.simple_pattern"
+    let simple_pattern2 = Gram.Entry.create "Command.simple_pattern2"
+    let simple_pattern_list =
+	 Gram.Entry.create "Command.simple_pattern_list"
+    let ucommand = snd (get_univ "command")
+  end
+
+
+module Tactic =
+  struct
+    let utactic = snd (get_univ "tactic")
+    let gec s =
+      let e = Gram.Entry.create ("Tactic." ^ s) in
+      Hashtbl.add utactic s (Ast e); e
+    
+    let gec_list s =
+      let e = Gram.Entry.create ("Tactic." ^ s) in
+      Hashtbl.add utactic s (ListAst e); e
+    
+    let binding_list = gec "binding_list"
+    let com_binding_list = gec_list "com_binding_list"
+    let comarg = gec "comarg"
+    let comarg_binding_list = gec_list "comarg_binding_list"
+    let numarg_binding_list = gec_list "numarg_binding_list"
+    let lcomarg_binding_list = gec_list "lcomarg_binding_list"
+    let comarg_list = gec_list "comarg_list"
+    let identarg = gec "identarg"
+    let lcomarg = gec "lcomarg"
+    let clausearg = gec "clausearg"
+    let ne_identarg_list = gec_list "ne_identarg_list"
+    let ne_num_list = gec_list "ne_num_list"
+    let ne_pattern_list = gec_list "ne_pattern_list"
+    let ne_pattern_hyp_list = gec_list "ne_pattern_hyp_list"
+    let one_intropattern = gec "one_intropattern"
+    let intropattern = gec "intropattern"
+    let ne_intropattern = gec "ne_intropattern"
+    let simple_intropattern = gec "simple_intropattern"
+    let ne_unfold_occ_list = gec_list "ne_unfold_occ_list"
+    let red_tactic = gec "red_tactic"
+    let red_flag = gec "red_flag"
+    let autoarg_depth = gec "autoarg_depth"
+    let autoarg_excluding = gec "autoarg_excluding"
+    let autoarg_adding = gec "autoarg_adding"
+    let autoarg_destructing = gec "autoarg_destructing"
+    let autoarg_usingTDB = gec "autoarg_usingTDB"
+    let numarg = gec "numarg"
+    let pattern_occ = gec "pattern_occ"
+    let pattern_occ_hyp = gec "pattern_occ_hyp"
+    let simple_binding = gec "simple_binding"
+    let simple_binding_list = gec_list "simple_binding_list"
+    let simple_tactic = gec "simple_tactic"
+    let tactic = gec "tactic"
+    let tactic_com = gec "tactic_com"
+    let tactic_com_list = gec "tactic_com_list"
+    let tactic_com_tail = gec "tactic_com_tail"
+    let unfold_occ = gec "unfold_occ"
+    let with_binding_list = gec "with_binding_list"
+    let fixdecl = gec_list "fixdecl"
+    let cofixdecl = gec_list "cofixdecl"
+    let tacarg_list = gec_list "tacarg_list"
+    let tactic_eoi = eoi_entry tactic
+  end
+
+
+module Vernac =
+  struct
+    let uvernac = snd (get_univ "vernac")
+    let gec s =
+      let e = Gram.Entry.create ("Vernac." ^ s) in
+      Hashtbl.add uvernac s (Ast e); e
+    
+    let gec_list s =
+      let e = Gram.Entry.create ("Vernac." ^ s) in
+      Hashtbl.add uvernac s (ListAst e); e
+    
+    let binder = gec "binder"
+    let block = gec_list "block"
+    let block_old_style = gec_list "block_old_style"
+    let comarg = gec "comarg"
+    let def_tok = gec "def_tok"
+    let definition_tail  = gec "definition_tail"
+    let dep = gec "dep"
+    let destruct_location = gec "destruct_location"
+    let check_tok = gec "check_tok"
+    let extracoindblock = gec_list "extracoindblock"
+    let extraindblock = gec_list "extraindblock"
+    let field = gec "field"
+    let nefields = gec_list "nefields"
+    let fields = gec "fields"
+    let destruct_location = gec "destruct_location"
+    let finite_tok = gec "finite_tok"
+    let grammar_entry_arg = gec "grammar_entry_arg"
+    let hyp_tok = gec "hyp_tok"
+    let hyps_tok = gec "hyps_tok"
+    let idcom = gec "idcom"
+    let identarg = gec "identarg"
+    let import_tok = gec "import_tok"
+    let indpar = gec "indpar"
+    let lcomarg = gec "lcomarg"
+    let lidcom = gec "lidcom"
+    let orient=gec "orient"
+    let lvernac = gec_list "lvernac"
+    let meta_binding = gec "meta_binding"
+    let meta_binding_list = gec_list "meta_binding_list"
+    let ne_binder_semi_list = gec_list "ne_binder_semi_list"
+    let ne_comarg_list = gec_list "ne_comarg_list"
+    let ne_identarg_comma_list = gec_list "ne_identarg_comma_list"
+    let identarg_list = gec_list "identarg_list"
+    let ne_identarg_list = gec_list "ne_identarg_list"
+    let ne_lidcom = gec_list "ne_lidcom"
+    let ne_numarg_list = gec_list "ne_numarg_list"
+    let ne_stringarg_list = gec_list "ne_stringarg_list"
+    let numarg = gec "numarg"
+    let numarg_list = gec_list "numarg_list"
+    let onecorec = gec "onecorec"
+    let oneind = gec "oneind"
+    let oneind_old_style = gec "oneind_old_style"
+    let onerec = gec "onerec"
+    let onescheme = gec "onescheme"
+    let opt_identarg_list = gec_list "opt_identarg_list"
+    let rec_constr = gec "rec_constr"
+    let record_tok = gec "record_tok"
+    let option_value = gec "option_value"
+    let param_tok = gec "param_tok"
+    let params_tok = gec "params_tok"
+    let sortdef = gec "sortdef"
+    let specif_tok = gec "specif_tok"
+    let specifcorec = gec_list "specifcorec"
+    let specifrec = gec_list "specifrec"
+    let specifscheme = gec_list "specifscheme"
+    let stringarg = gec "stringarg"
+    let tacarg = gec "tacarg"
+    let theorem_body = gec "theorem_body"
+    let theorem_body_line = gec "theorem_body_line"
+    let theorem_body_line_list = gec_list "theorem_body_line_list"
+    let thm_tok = gec "thm_tok"
+    let varg_ne_stringarg_list = gec "varg_ne_stringarg_list"
+    let vernac = gec "vernac"
+    let vernac_eoi = eoi_entry vernac
+  end
+
+
+module Prim =
+  struct
+    let uprim = snd (get_univ "prim")
+    let gec s =
+      let e = Gram.Entry.create ("Prim." ^ s) in
+      	Hashtbl.add uprim s (Ast e); e
+    let ast = gec "ast"
+    let ast_eoi = eoi_entry ast
+    let astact = gec "astact"
+    let astpat = gec "astpat"
+    let entry_type = gec "entry_type"
+    let grammar_entry = gec "grammar_entry"
+    let grammar_entry_eoi = eoi_entry grammar_entry
+    let ident = gec "ident"
+    let number = gec "number"
+    let path = gec "path"
+    let string = gec "string"
+    let syntax_entry = gec "syntax_entry"
+    let syntax_entry_eoi = eoi_entry syntax_entry
+    let uprim = snd (get_univ "prim")
+    let var = gec "var"
+  end
+
+
+let main_entry = Gram.Entry.create "vernac"
+
+GEXTEND Gram
+  main_entry:
+    [ [ a = Vernac.vernac -> Some a | EOI -> None ] ]
+  ;
+END
+
+(* Quotations *)
+
+open Prim
+let define_quotation default s e =
+  (if default then
+    GEXTEND Gram
+      ast: [ [ "<<"; c = e; ">>" -> c ] ];
+   END);
+  (GEXTEND Gram
+     ast:
+       [ [ "<"; ":"; LIDENT $s$; ":"; "<"; c = e; ">>" -> c ] ];
+   END)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
new file mode 100644
index 000000000..5bd9a31da
--- /dev/null
+++ b/parsing/pcoq.mli
@@ -0,0 +1,228 @@
+
+(* $Id$ *)
+
+(* The lexer and parser of Coq. *)
+
+val lexer : Token.lexer
+
+module Gram : Grammar.S
+
+type typed_entry =
+  | Ast of Coqast.t Gram.Entry.e
+  | ListAst of Coqast.t list Gram.Entry.e
+
+val grammar_extend :
+  typed_entry -> Gramext.position option ->
+    (string option * Gramext.g_assoc option *
+     (Gramext.g_symbol list * Gramext.g_action) list) list
+    -> unit
+
+val remove_grammars : int -> unit
+
+(* Parse a string *)
+
+val parse_string : 'a Gram.Entry.e -> string -> 'a
+val eoi_entry : 'a Gram.Entry.e -> 'a Gram.Entry.e
+val map_entry : ('a -> 'b) -> 'a Gram.Entry.e -> 'b Gram.Entry.e
+
+val slam_ast : Coqast.loc -> Coqast.t -> Coqast.t -> Coqast.t
+
+(* Entry types *)
+
+type entry_type = ETast | ETastl
+
+val entry_type : Coqast.t -> entry_type
+val type_of_entry : typed_entry -> entry_type
+
+(* Table of Coq's grammar entries *)
+
+type gram_universe
+
+val get_univ : string -> string * gram_universe
+val get_entry :  string * gram_universe -> string -> typed_entry
+
+val create_entry : string * gram_universe -> string -> entry_type ->
+  typed_entry
+val force_entry_type : string * gram_universe -> string ->
+  entry_type -> typed_entry
+
+(* Quotations *)
+
+val define_quotation : bool -> string -> (Coqast.t Gram.Entry.e) -> unit
+
+(* The main entry: reads an optional vernac command *)
+
+val main_entry : Coqast.t option Gram.Entry.e
+
+(* Initial state of the grammar *)
+
+module Command :
+  sig
+    val abstraction_tail : Coqast.t Gram.Entry.e
+    val binder : Coqast.t Gram.Entry.e
+    val cofixbinder : Coqast.t Gram.Entry.e
+    val cofixbinders : Coqast.t list Gram.Entry.e
+    val command : Coqast.t Gram.Entry.e
+    val command0 : Coqast.t Gram.Entry.e
+    val command1 : Coqast.t Gram.Entry.e
+    val command10 : Coqast.t Gram.Entry.e
+    val command2 : Coqast.t Gram.Entry.e
+    val command3 : Coqast.t Gram.Entry.e
+    val command5 : Coqast.t Gram.Entry.e
+    val command6 : Coqast.t Gram.Entry.e
+    val command7 : Coqast.t Gram.Entry.e
+    val command8 : Coqast.t Gram.Entry.e
+    val command9 : Coqast.t Gram.Entry.e
+    val command91 : Coqast.t Gram.Entry.e
+    val command_eoi : Coqast.t Gram.Entry.e
+    val equation : Coqast.t Gram.Entry.e
+    val fixbinder : Coqast.t Gram.Entry.e
+    val fixbinders : Coqast.t list Gram.Entry.e
+    val ident : Coqast.t Gram.Entry.e
+    val lassoc_command4 : Coqast.t Gram.Entry.e
+    val lcommand : Coqast.t Gram.Entry.e
+    val lsimple_pattern : (string list * Coqast.t) Gram.Entry.e
+    val ne_binder_list : Coqast.t list Gram.Entry.e
+    val ne_command91_list : Coqast.t list Gram.Entry.e
+    val ne_command9_list : Coqast.t list Gram.Entry.e
+    val ne_command_list : Coqast.t list Gram.Entry.e
+    val ne_eqn_list : Coqast.t list Gram.Entry.e
+    val ne_ident_comma_list : Coqast.t list Gram.Entry.e
+    val ne_pattern_list : (string list * Coqast.t list) Gram.Entry.e
+    val pattern : (string list * Coqast.t) Gram.Entry.e
+    val pattern_list : (string list * Coqast.t list) Gram.Entry.e
+    val product_tail : Coqast.t Gram.Entry.e
+    val raw_command : Coqast.t Gram.Entry.e
+    val simple_pattern : (string list * Coqast.t) Gram.Entry.e
+    val simple_pattern2 : (string list * Coqast.t) Gram.Entry.e
+    val simple_pattern_list : (string list * Coqast.t list) Gram.Entry.e
+  end
+
+module Tactic :
+  sig
+    val autoarg_adding : Coqast.t Gram.Entry.e
+    val autoarg_depth : Coqast.t Gram.Entry.e
+    val autoarg_destructing : Coqast.t Gram.Entry.e
+    val autoarg_excluding : Coqast.t Gram.Entry.e
+    val autoarg_usingTDB : Coqast.t Gram.Entry.e
+    val binding_list : Coqast.t Gram.Entry.e
+    val clausearg : Coqast.t Gram.Entry.e
+    val cofixdecl : Coqast.t list Gram.Entry.e
+    val com_binding_list : Coqast.t list Gram.Entry.e
+    val comarg : Coqast.t Gram.Entry.e
+    val comarg_binding_list : Coqast.t list Gram.Entry.e
+    val comarg_list : Coqast.t list Gram.Entry.e
+    val fixdecl : Coqast.t list Gram.Entry.e
+    val identarg : Coqast.t Gram.Entry.e
+    val intropattern : Coqast.t Gram.Entry.e
+    val lcomarg : Coqast.t Gram.Entry.e
+    val lcomarg_binding_list : Coqast.t list Gram.Entry.e
+    val ne_identarg_list : Coqast.t list Gram.Entry.e
+    val ne_intropattern : Coqast.t Gram.Entry.e
+    val ne_num_list : Coqast.t list Gram.Entry.e
+    val ne_pattern_list : Coqast.t list Gram.Entry.e
+    val ne_pattern_hyp_list : Coqast.t list Gram.Entry.e
+    val ne_unfold_occ_list : Coqast.t list Gram.Entry.e
+    val numarg : Coqast.t Gram.Entry.e
+    val numarg_binding_list : Coqast.t list Gram.Entry.e
+    val one_intropattern : Coqast.t Gram.Entry.e
+    val pattern_occ : Coqast.t Gram.Entry.e
+    val pattern_occ_hyp : Coqast.t Gram.Entry.e
+    val red_flag : Coqast.t Gram.Entry.e
+    val red_tactic : Coqast.t Gram.Entry.e
+    val simple_binding : Coqast.t Gram.Entry.e
+    val simple_binding_list : Coqast.t list Gram.Entry.e
+    val simple_intropattern : Coqast.t Gram.Entry.e
+    val simple_tactic : Coqast.t Gram.Entry.e
+    val tactic : Coqast.t Gram.Entry.e
+    val tactic_com : Coqast.t Gram.Entry.e
+    val tactic_com_list : Coqast.t Gram.Entry.e
+    val tactic_com_tail : Coqast.t Gram.Entry.e
+    val tactic_eoi : Coqast.t Gram.Entry.e
+    val unfold_occ : Coqast.t Gram.Entry.e
+    val with_binding_list : Coqast.t Gram.Entry.e
+  end
+
+module Vernac :
+  sig
+    val binder : Coqast.t Gram.Entry.e
+    val block : Coqast.t list Gram.Entry.e
+    val block_old_style : Coqast.t list Gram.Entry.e
+    val check_tok : Coqast.t Gram.Entry.e
+    val comarg : Coqast.t Gram.Entry.e
+    val def_tok : Coqast.t Gram.Entry.e
+    val definition_tail : Coqast.t Gram.Entry.e
+    val dep : Coqast.t Gram.Entry.e
+    val destruct_location : Coqast.t Gram.Entry.e
+    val destruct_location : Coqast.t Gram.Entry.e
+    val extracoindblock : Coqast.t list Gram.Entry.e
+    val extraindblock : Coqast.t list Gram.Entry.e
+    val field : Coqast.t Gram.Entry.e
+    val fields : Coqast.t Gram.Entry.e
+    val finite_tok : Coqast.t Gram.Entry.e
+    val hyp_tok : Coqast.t Gram.Entry.e
+    val hyps_tok : Coqast.t Gram.Entry.e
+    val idcom : Coqast.t Gram.Entry.e
+    val identarg : Coqast.t Gram.Entry.e
+    val import_tok : Coqast.t Gram.Entry.e
+    val indpar : Coqast.t Gram.Entry.e
+    val lcomarg : Coqast.t Gram.Entry.e
+    val lidcom : Coqast.t Gram.Entry.e
+    val orient:Coqast.t Gram.Entry.e;; 
+    val lvernac : Coqast.t list Gram.Entry.e
+    val meta_binding : Coqast.t Gram.Entry.e
+    val meta_binding_list : Coqast.t list Gram.Entry.e
+    val ne_binder_semi_list : Coqast.t list Gram.Entry.e
+    val ne_comarg_list : Coqast.t list Gram.Entry.e
+    val ne_identarg_comma_list : Coqast.t list Gram.Entry.e
+    val ne_identarg_list : Coqast.t list Gram.Entry.e
+    val ne_lidcom : Coqast.t list Gram.Entry.e
+    val ne_numarg_list : Coqast.t list Gram.Entry.e
+    val ne_stringarg_list : Coqast.t list Gram.Entry.e
+    val nefields : Coqast.t list Gram.Entry.e
+    val numarg : Coqast.t Gram.Entry.e
+    val numarg_list : Coqast.t list Gram.Entry.e
+    val onecorec : Coqast.t Gram.Entry.e
+    val oneind : Coqast.t Gram.Entry.e
+    val oneind_old_style : Coqast.t Gram.Entry.e
+    val onerec : Coqast.t Gram.Entry.e
+    val onescheme : Coqast.t Gram.Entry.e
+    val opt_identarg_list : Coqast.t list Gram.Entry.e
+    val option_value : Coqast.t Gram.Entry.e
+    val param_tok : Coqast.t Gram.Entry.e
+    val params_tok : Coqast.t Gram.Entry.e
+    val rec_constr : Coqast.t Gram.Entry.e
+    val record_tok : Coqast.t Gram.Entry.e
+    val sortdef : Coqast.t Gram.Entry.e
+    val specif_tok : Coqast.t Gram.Entry.e
+    val specifcorec : Coqast.t list Gram.Entry.e
+    val specifrec : Coqast.t list Gram.Entry.e
+    val specifscheme : Coqast.t list Gram.Entry.e
+    val stringarg : Coqast.t Gram.Entry.e
+    val tacarg : Coqast.t Gram.Entry.e
+    val theorem_body : Coqast.t Gram.Entry.e
+    val theorem_body_line : Coqast.t Gram.Entry.e
+    val theorem_body_line_list : Coqast.t list Gram.Entry.e
+    val thm_tok : Coqast.t Gram.Entry.e
+    val varg_ne_stringarg_list : Coqast.t Gram.Entry.e
+    val vernac : Coqast.t Gram.Entry.e
+    val vernac_eoi : Coqast.t Gram.Entry.e
+  end
+
+module Prim :
+  sig
+    val ast : Coqast.t Gram.Entry.e
+    val ast_eoi : Coqast.t Gram.Entry.e
+    val astact : Coqast.t Gram.Entry.e
+    val astpat: Coqast.t Gram.Entry.e
+    val entry_type : Coqast.t Gram.Entry.e
+    val grammar_entry : Coqast.t Gram.Entry.e
+    val grammar_entry_eoi : Coqast.t Gram.Entry.e
+    val ident : Coqast.t Gram.Entry.e
+    val number : Coqast.t Gram.Entry.e
+    val path : Coqast.t Gram.Entry.e
+    val string : Coqast.t Gram.Entry.e
+    val syntax_entry : Coqast.t Gram.Entry.e
+    val syntax_entry_eoi : Coqast.t Gram.Entry.e
+    val var : Coqast.t Gram.Entry.e
+  end