1 files changed, 60 insertions, 28 deletions

diff --git a/parsing/ast.mli b/parsing/ast.mli
index fae49ac34..fd7581199 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -11,13 +11,17 @@
 (*i*)
 open Pp
 open Names
-open Pcoq
+open Coqast
+open Genarg
 (*i*)
 
 (* Abstract syntax trees. *)
 
 val dummy_loc : Coqast.loc
 val loc : Coqast.t -> Coqast.loc
+(*
+val vernac_loc : Coqast.vernac_ast -> Coqast.loc
+*)
 
 (* ast constructors with dummy location *)
 val ope : string * Coqast.t list -> Coqast.t
@@ -38,43 +42,70 @@ val section_path : section_path -> section_path
 val num_of_ast : Coqast.t -> int
 val id_of_ast : Coqast.t -> string
 val nvar_of_ast : Coqast.t -> identifier
+val meta_of_ast : Coqast.t -> string
 
 (* ast processing datatypes *)
 
+type entry_type =
+  | PureAstType
+  | IntAstType
+  | IdentAstType
+  | AstListType
+  | TacticAtomAstType
+  | ThmTokenAstType
+  | DynamicAstType
+  | ReferenceAstType
+  | GenAstType of Genarg.argument_type
+
 (* patterns of ast *)
-type pat =
-  | Pquote of Coqast.t
+type astpat =
+  | Pquote of t
   | Pmeta of string * tok_kind
   | Pnode of string * patlist
-  | Pslam of identifier option * pat
-  | Pmeta_slam of string * pat
+  | Pslam of identifier option * astpat
+  | Pmeta_slam of string * astpat
 
 and patlist =
-  | Pcons of pat * patlist
+  | Pcons of astpat * patlist
   | Plmeta of string
   | Pnil
 
 and tok_kind = Tnum | Tid | Tstr | Tpath | Tvar | Tany | Tlist
 
+type pat =
+  | AstListPat of patlist
+  | PureAstPat of astpat
+
 (* 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
+  | Act of pat
+  | ActCase of act * (pat * act) list
+  | ActCaseList of act * (pat * act) list
 
 (* values associated to variables *)
-type v =
-  | Vast of Coqast.t
-  | Vastlist of Coqast.t list
+type typed_ast =
+  | AstListNode of Coqast.t list
+  | PureAstNode of Coqast.t
+
+type ast_action_type = ETast | ETastl
+
+type grammar_action =
+  | SimpleAction of loc * typed_ast
+  | CaseAction of
+      loc * grammar_action * ast_action_type * (t list * grammar_action) list
 
-type env = (string * v) list
+type env = (string * typed_ast) list
 
 val coerce_to_var : Coqast.t -> Coqast.t 
 
-(*
 val coerce_to_id : Coqast.t -> identifier
-*)
+
+val coerce_qualid_to_id : Nametab.qualid Util.located -> identifier
+
+val coerce_reference_to_id : Tacexpr.reference_expr -> identifier
+
+val abstract_binders_ast :
+  Coqast.loc -> string -> Coqast.t -> Coqast.t -> Coqast.t
 
 exception No_match of string
 
@@ -82,35 +113,36 @@ 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_astpat : astpat -> std_ppcmds
 val print_astlpat : patlist -> std_ppcmds
 
 (* Meta-syntax operations: matching and substitution *)
 
-type entry_env = (string * entry_type) list
+type entry_env = (string * ast_action_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 pat_sub : Coqast.loc -> env -> astpat -> Coqast.t
+val val_of_ast : entry_env -> Coqast.t -> astpat
 val vall_of_astl : entry_env -> Coqast.t list -> patlist
 
+val pat_of_ast : entry_env -> Coqast.t -> astpat * entry_env
+
 val alpha_eq : Coqast.t * Coqast.t -> bool
-val alpha_eq_val : v * v -> bool
+val alpha_eq_val : typed_ast * typed_ast -> bool
 
 val occur_var_ast : identifier -> Coqast.t -> bool
 val replace_vars_ast : (identifier * identifier) list -> Coqast.t -> Coqast.t
 
-val bind_env : env -> string -> v -> env
-val ast_match : env -> pat -> Coqast.t -> env
+val bind_env : env -> string -> typed_ast -> env
+val ast_match : env -> astpat -> 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_match : ('a -> astpat) -> env -> 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 to_pat : entry_env -> Coqast.t -> (astpat * entry_env)
 
-val eval_act : Coqast.loc -> env -> act -> v
-val to_act_check_vars : entry_env -> entry_type -> Coqast.t -> act
+val eval_act : Coqast.loc -> env -> act -> typed_ast
+val to_act_check_vars : entry_env -> ast_action_type -> grammar_action -> act