diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-09 02:47:14 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-09 02:47:14 +0000 |
| commit | 4b71b4bfc7b5a0316f549a88fa6495acde9d27c5 (patch) | |
| tree | 1e26b4ab3841747c0cb7674e7f0c2e7d65b1146b | |
| parent | 7d8b5d561ac3003ded12a66b884e0cdb9659087f (diff) | |
pp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3390 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/ocaml.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index f168c57b8..56108a225 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -365,8 +365,8 @@ let pp_logical_ind ip packet = let pp_singleton kn packet = let l = rename_tvars keywords packet.ip_vars in - hov 0 (str "type " ++ spc () ++ pp_parameters l ++ - pp_global (IndRef (kn,0)) ++ spc () ++ str "=" ++ spc () ++ + hov 0 (str "type " ++ pp_parameters l ++ + pp_global (IndRef (kn,0)) ++ str " =" ++ spc () ++ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ pp_comment (str "singleton inductive, whose constructor was " ++ Printer.pr_global (ConstructRef ((kn,0),1)))) |