Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

1 files changed, 0 insertions, 47 deletions

diff --git a/dev/doc/ast.ml b/dev/doc/ast.ml
deleted file mode 100644
index 2153ef47..00000000
--- a/dev/doc/ast.ml
+++ /dev/null
@@ -1,47 +0,0 @@
-
-type constr_ast =
-  Pair of constr_ast * constr_ast
-| Prod of binder list * constr_ast
-| Lambda of binder list * constr_ast
-| Let of string * constr_ast * constr_ast
-| LetCase of binder list * constr_ast * constr_ast
-| IfCase of constr_ast * constr_ast * constr_ast
-| Eval of red_fun * constr_ast
-| Infix of string * constr_ast * constr_ast
-| Prefix of string * constr_ast
-| Postfix of string * constr_ast
-| Appl of constr_ast * constr_arg list
-| ApplExpl of string list * constr_ast list
-| Scope of string * constr_ast
-| Qualid of string list
-| Prop | Set | Type
-| Int of string
-| Hole
-| Meta of string
-| Fixp of fix_kind *
-      (string * binder list * constr_ast * string option * constr_ast) list *
-      string
-| Match of case_item list * constr_ast option *
-           (pattern list * constr_ast) list 
-
-and red_fun = Simpl
-
-and binder = string * constr_ast
-
-and constr_arg = string option * constr_ast
-
-and fix_kind = Fix | CoFix
-
-and case_item = constr_ast * (string option * constr_ast option)
-
-and pattern = 
-  PatAs of pattern * string
-| PatType of pattern * constr_ast
-| PatConstr of string * pattern list
-| PatVar of string
-
-let mk_cast c t =
-  if t=Hole then c else Infix(":",c,t)
-
-let mk_lambda bl t =
-  if bl=[] then t else Lambda(bl,t)