1 files changed, 58 insertions, 0 deletions
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
index a304aa06b3..817ccb5cd3 100644
--- a/parsing/coqast.mli
+++ b/parsing/coqast.mli
@@ -50,3 +50,61 @@ 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
+
+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