1 files changed, 1 insertions, 61 deletions
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
index 52b19c6bc..5b8c9d7d7 100644
--- a/parsing/coqast.mli
+++ b/parsing/coqast.mli
@@ -9,14 +9,13 @@
 (*i $Id$ i*)
 
 (*i*)
+open Util
 open Names
 open Libnames
 (*i*)
 
 (* Abstract syntax trees. *)
 
-type loc = int * int
-
 type t =
   | Node of loc * string * t list
   | Nmeta of loc * string
@@ -50,62 +49,3 @@ val fold_tactic_expr :
   ('a -> t -> 'a) -> ('a -> tactic_expr -> 'a) -> 'a -> tactic_expr -> 'a
 val iter_tactic_expr : (tactic_expr -> unit) -> tactic_expr -> unit
 *)
-
-
-open Util
-open Rawterm
-open Term
-
-type scope_name = string
-
-type reference_expr = 
-  | RQualid of qualid located
-  | RIdent of identifier located
-
-type explicitation = int
-
-type cases_pattern =
-  | CPatAlias of loc * cases_pattern * identifier
-  | CPatCstr of loc * reference_expr * cases_pattern list
-  | CPatAtom of loc * reference_expr option
-  | CPatNumeral of loc * Bignat.bigint
-  | CPatDelimiters of loc * scope_name * cases_pattern
-
-type ordered_case_style = CIf | CLet | CMatch | CCase
-
-type constr_ast =
-  | CRef of reference_expr
-  | CFix of loc * identifier located * fixpoint_expr list
-  | CCoFix of loc * identifier located * cofixpoint_expr list
-  | CArrow of loc * constr_ast * constr_ast
-  | CProdN of loc * (name located list * constr_ast) list * constr_ast
-  | CLambdaN of loc * (name located list * constr_ast) list * constr_ast
-  | CLetIn of loc * identifier located * constr_ast * constr_ast
-  | CAppExpl of loc * reference_expr * constr_ast list
-  | CApp of loc * constr_ast * (constr_ast * explicitation option) list
-  | CCases of loc * case_style * constr_ast option * constr_ast list *
-      (loc * cases_pattern list * constr_ast) list
-  | COrderedCase of loc * ordered_case_style * constr_ast option * constr_ast * constr_ast list
-  | CHole of loc
-  | CMeta of loc * int
-  | CSort of loc * rawsort
-  | CCast of loc * constr_ast * constr_ast
-  | CNotation of loc * string * constr_ast list
-  | CNumeral of loc * Bignat.bigint
-  | CDelimiters of loc * scope_name * constr_ast
-  | CDynamic of loc * Dyn.t
-
-and local_binder = name located list * constr_ast 
-
-and fixpoint_expr = identifier * local_binder list * constr_ast * constr_ast
-
-and cofixpoint_expr = identifier * constr_ast * constr_ast
-
-val constr_loc : constr_ast -> loc
-
-val cases_pattern_loc : cases_pattern -> loc
-
-val replace_vars_constr_ast :
-  (identifier * identifier) list -> constr_ast -> constr_ast
-
-val occur_var_constr_ast : identifier -> constr_ast -> bool