aboutsummaryrefslogtreecommitdiffstats
path: root/src/common
diff options
context:
space:
mode:
Diffstat (limited to 'src/common')
-rw-r--r--src/common/Optionmonad.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/common/Optionmonad.v b/src/common/Optionmonad.v
index 037dd83..8112eb9 100644
--- a/src/common/Optionmonad.v
+++ b/src/common/Optionmonad.v
@@ -70,8 +70,7 @@ Module Option <: Monad.
End Option.
Module OptionExtra.
- Module OE := MonadExtra(Option).
- Export OE.
+ Module Export OE := MonadExtra(Option).
Lemma mfold_left_Some :
forall A B f x n y,