diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-30 01:20:28 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-30 01:20:28 +0000 |
| commit | 300dd33e3d35fbab6fbeadb8e4450cc41c5a6276 (patch) | |
| tree | c1bb948462c2b97c9da3a84ae4c5bf4905479655 /contrib/extraction/ocaml.ml | |
| parent | 24eaf1786c93f8e2db0b41d15eef2b92c944c169 (diff) | |
fignolage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3625 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/ocaml.ml')
| -rw-r--r-- | contrib/extraction/ocaml.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index e51936652..1d6b40372 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -478,7 +478,7 @@ let pp_decl mp = (str "let " ++ if is_custom r then e ++ str " = " ++ str (find_custom r) - else if is_projection r then e ++ str " x = x." ++ e ++ fnl () + else if is_projection r then e ++ str " x = x." ++ e else pp_function (empty_env ()) e a) | Dfix (rv,defs,typs) -> pp_Dfix true 0 (rv,defs,typs) |