diff options
author | 2010-04-29 09:56:37 +0000 | |
---|---|---|
committer | 2010-04-29 09:56:37 +0000 | |
commit | f73d7c4614d000f068550b5144d80b7eceed58e9 (patch) | |
tree | 4fa9a679a6e55269cc5c7cf24fce725acb2574b5 /dev/ocamlweb-doc/ast.ml | |
parent | 552e596e81362e348fc17fcebcc428005934bed6 (diff) |
Move from ocamlweb to ocamdoc to generate mli documentation
dev/ocamlweb-doc has been erased. I hope no one still use the
"new-parse" it generate.
In dev/,
make html will generate in dev/html/ "clickable version of mlis". (as
the caml standard library)
make coq.pdf will generate nearly the same awfull stuff that coq.ps was.
make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of
the given directory.
ocamldoc comment syntax is here :
http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html
The possibility to put graphs in pdf/html seems to be lost.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/ocamlweb-doc/ast.ml')
-rw-r--r-- | dev/ocamlweb-doc/ast.ml | 47 |
1 files changed, 0 insertions, 47 deletions
diff --git a/dev/ocamlweb-doc/ast.ml b/dev/ocamlweb-doc/ast.ml deleted file mode 100644 index 4eb135d83..000000000 --- a/dev/ocamlweb-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) |