aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/scheme.ml
diff options
context:
space:
mode:
authorPierre Letouzey2015-04-09 14:46:37 +0200
committerPierre Letouzey2015-04-09 14:46:37 +0200
commit429f493997e34bfaac930c68bf6b267a5b9640ee (patch)
tree28f15d0aeff2ce899a312f31e10fe2030b2dd813 /plugins/extraction/scheme.ml
parentaeec29a177e8f1c89996c0449e4cd81ca3ca4377 (diff)
parenteaa3f9719d6190ba92ce55816f11c70b30434309 (diff)
Merge branch 'v8.5' into trunk
Diffstat (limited to 'plugins/extraction/scheme.ml')
-rw-r--r--plugins/extraction/scheme.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 99b4fd448d..cc8b6d8e79 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -212,7 +212,7 @@ and pp_module_expr = function
| MEfunctor _ -> mt ()
(* for the moment we simply discard unapplied functors *)
| MEident _ | MEapply _ -> assert false
- (* should be expansed in extract_env *)
+ (* should be expanded in extract_env *)
let pp_struct =
let pp_sel (mp,sel) =