diff options
| author | letouzey | 2009-03-24 17:46:31 +0000 |
|---|---|---|
| committer | letouzey | 2009-03-24 17:46:31 +0000 |
| commit | e0bd95f7c3e0304506d62a900ae26c58ec3d4f38 (patch) | |
| tree | 24731b56e8d50ed5b30e73f1ce7bf0d7ed198420 /tools | |
| parent | 89ed0ae86a32572e1348519990a734697e7080a3 (diff) | |
pretty.mll of coqdoc becomes cpretty.mll (avoid clash with a camlp5 file)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12011 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/cpretty.mli (renamed from tools/coqdoc/pretty.mli) | 0 | ||||
| -rw-r--r-- | tools/coqdoc/cpretty.mll (renamed from tools/coqdoc/pretty.mll) | 0 | ||||
| -rw-r--r-- | tools/coqdoc/main.ml | 4 |
3 files changed, 2 insertions, 2 deletions
diff --git a/tools/coqdoc/pretty.mli b/tools/coqdoc/cpretty.mli index f02a79be50..f02a79be50 100644 --- a/tools/coqdoc/pretty.mli +++ b/tools/coqdoc/cpretty.mli diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/cpretty.mll index 1420c9a924..1420c9a924 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/cpretty.mll diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 24538360a2..bbfd93fd44 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -383,7 +383,7 @@ let copy src dst = let gen_one_file l = let file = function | Vernac_file (f,m) -> - Output.set_module m; Pretty.coq_file f m + Output.set_module m; Cpretty.coq_file f m | Latex_file _ -> () in if (!header_trailer) then Output.header (); @@ -399,7 +399,7 @@ let gen_mult_files l = let hf = target_full_name m in open_out_file hf; if (!header_trailer) then Output.header (); - Pretty.coq_file f m; + Cpretty.coq_file f m; if (!header_trailer) then Output.trailer (); close_out_file() | Latex_file _ -> () |