diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/ocaml.ml | 5 | ||||
| -rw-r--r-- | plugins/ltac/LtacDummy.v | 2 | ||||
| -rw-r--r-- | plugins/ltac/ltac_dummy.ml | 0 | ||||
| -rw-r--r-- | plugins/ltac/ltac_dummy.mli | 0 | ||||
| -rw-r--r-- | plugins/ltac/ltac_plugin.mlpack | 1 | ||||
| -rw-r--r-- | plugins/ltac/vo.itarget | 1 |
6 files changed, 7 insertions, 2 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 1c29a9bc24..5d10cb939d 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -618,12 +618,13 @@ let rec pp_specif = function with Not_found -> pp_spec s) | (l,Smodule mt) -> let def = pp_module_type [] mt in - let def' = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++ (try let ren = Common.check_duplicate (top_visible_mp ()) l in - fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def') + fnl () ++ + hov 1 (str ("module "^ren^" :") ++ spc () ++ + str "module type of struct include " ++ name ++ str " end") with Not_found -> Pp.mt ()) | (l,Smodtype mt) -> let def = pp_module_type [] mt in diff --git a/plugins/ltac/LtacDummy.v b/plugins/ltac/LtacDummy.v new file mode 100644 index 0000000000..4f96bbaeb9 --- /dev/null +++ b/plugins/ltac/LtacDummy.v @@ -0,0 +1,2 @@ +(* The sole reason of this file is to trick coq's build system to build the dummy ltac plugin *) +Declare ML Module "ltac_plugin". diff --git a/plugins/ltac/ltac_dummy.ml b/plugins/ltac/ltac_dummy.ml new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/plugins/ltac/ltac_dummy.ml diff --git a/plugins/ltac/ltac_dummy.mli b/plugins/ltac/ltac_dummy.mli new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/plugins/ltac/ltac_dummy.mli diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack new file mode 100644 index 0000000000..6efb477cce --- /dev/null +++ b/plugins/ltac/ltac_plugin.mlpack @@ -0,0 +1 @@ +Ltac_dummy diff --git a/plugins/ltac/vo.itarget b/plugins/ltac/vo.itarget new file mode 100644 index 0000000000..4eff76566a --- /dev/null +++ b/plugins/ltac/vo.itarget @@ -0,0 +1 @@ +LtacDummy.vo |