aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/haskell.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-07-02 13:36:05 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-07-02 13:36:05 +0000
commit68a133db448e5663da6daf677d4d882bf1bad05c (patch)
treeaa3255a91f59ef9a2d7f5a9e9055165b6f5121be /plugins/extraction/haskell.ml
parentdacb4b76afe554f1a1e17d981bc98d9fc3a8e807 (diff)
Extraction: no more MPself hence no need for subst during pp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13235 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/haskell.ml')
-rw-r--r--plugins/extraction/haskell.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index c199225e4..333bdcddd 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -325,7 +325,7 @@ and pp_module_expr = function
let pp_struct =
let pp_sel (mp,sel) =
- push_visible mp None;
+ push_visible mp;
let p = prlist_strict pp_structure_elem sel in
pop_visible (); p
in