aboutsummaryrefslogtreecommitdiff
path: root/bootstrap
diff options
context:
space:
mode:
Diffstat (limited to 'bootstrap')
-rw-r--r--bootstrap/Monads.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index 4c800d48c6..2aceb9fbc5 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -641,7 +641,7 @@ Module Logical.
End Logical.
-
+Set Extraction Flag 1007.
Set Extraction Conservative Types.
Set Extraction File Comment "
This file has been generated by extraction of bootstrap/Monad.v.