1 files changed, 0 insertions, 123 deletions
diff --git a/parsing/ast.mli b/parsing/ast.mli
deleted file mode 100755
index 7bc0b607..00000000
--- a/parsing/ast.mli
+++ /dev/null
@@ -1,123 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: ast.mli,v 1.17.2.1 2004/07/16 19:30:37 herbelin Exp $ i*)
-
-(*i*)
-open Pp
-open Util
-open Names
-open Libnames
-open Coqast
-open Topconstr
-open Genarg
-(*i*)
-
-(* Abstract syntax trees. *)
-
-val loc : Coqast.t -> loc
-
-(* ast constructors with dummy location *)
-val ope : string * Coqast.t list -> Coqast.t
-val slam : identifier option * Coqast.t -> Coqast.t
-val nvar : identifier -> Coqast.t
-val ide : string -> Coqast.t
-val num : int -> Coqast.t
-val string : string -> Coqast.t
-val path : kernel_name -> Coqast.t
-val dynamic : Dyn.t -> Coqast.t
-
-val set_loc : loc -> Coqast.t -> Coqast.t
-
-val path_section : loc -> kernel_name -> Coqast.t
-val section_path : kernel_name -> kernel_name
-
-(* ast destructors *)
-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
-
-(* patterns of ast *)
-type astpat =
-  | Pquote of t
-  | Pmeta of string * tok_kind
-  | Pnode of string * patlist
-  | Pslam of identifier option * astpat
-  | Pmeta_slam of string * astpat
-
-and 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 =
-  | Act of constr_expr
-  | ActCase of act * (pat * act) list
-  | ActCaseList of act * (pat * act) list
-
-(* values associated to variables *)
-type typed_ast =
-  | AstListNode of Coqast.t list
-  | PureAstNode of Coqast.t
-
-type ast_action_type = ETast | ETastl
-
-type dynamic_grammar =
-  | ConstrNode of constr_expr
-  | CasesPatternNode of cases_pattern_expr
-
-type grammar_action =
-  | SimpleAction of loc * dynamic_grammar
-  | CaseAction of
-      loc * grammar_action * ast_action_type * (t list * grammar_action) list
-
-type env = (string * typed_ast) list
-
-val coerce_to_id : constr_expr -> identifier located
-
-val coerce_global_to_id : reference -> identifier
-val coerce_reference_to_id : reference -> identifier
-
-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 : astpat -> std_ppcmds
-val print_astlpat : patlist -> std_ppcmds
-
-(* Meta-syntax operations: matching and substitution *)
-
-type entry_env = (string * ast_action_type) list
-
-val grammar_type_error : loc * string -> 'a
- 
-(* Converting and checking free meta-variables *)
-
-(* For old ast printer *)
-val pat_sub : loc -> env -> astpat -> Coqast.t
-val val_of_ast : entry_env -> Coqast.t -> astpat
-val alpha_eq : Coqast.t * Coqast.t -> bool
-val alpha_eq_val : typed_ast * typed_ast -> bool
-val occur_var_ast : identifier -> Coqast.t -> bool
-val find_all_matches : ('a -> astpat) -> env -> t -> 'a list -> ('a * env) list
-val first_matchl : ('a -> patlist) -> env -> Coqast.t list -> 'a list ->
-  ('a * env) option
-val to_pat : entry_env -> Coqast.t -> (astpat * entry_env)
-
-(* Object substitution in modules *)
-val subst_astpat : Names.substitution -> astpat -> astpat