diff options
| author | herbelin | 2006-05-23 21:51:59 +0000 |
|---|---|---|
| committer | herbelin | 2006-05-23 21:51:59 +0000 |
| commit | e24d8149c3aefd11b03458b6f9b3e38ca454b07a (patch) | |
| tree | 7c66dda6b63ea0c1f3e6e03259ef0b1609aca8b6 /dev/doc/ast.ml | |
| parent | b65fd67d6210f480eed759d58422ca8c4da95eab (diff) | |
Restructuration dossier dev et mise à jour de certaines documentations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8856 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/doc/ast.ml')
| -rw-r--r-- | dev/doc/ast.ml | 47 |
1 files changed, 0 insertions, 47 deletions
diff --git a/dev/doc/ast.ml b/dev/doc/ast.ml deleted file mode 100644 index 2153ef47c0..0000000000 --- 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) |