diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:37:16 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:37:16 +0000 |
| commit | df1f906cd0b729f95d409100ae1a86f898e6656b (patch) | |
| tree | baa01547f58fc0f132d6f6a43ad9222a92ebdcf8 /bootstrap | |
| parent | ab1859f7bac626704de49d1df9d9ee05c2538a5b (diff) | |
Set an extraction flag for inling let-s in Monad.v.
Reduces the size of split significantly. In particular it now uses only 2 matches instead of 4.
Patch by Pierre-Marie Pédrot and Pierre Letouzey.
Signed-off-by: Arnaud Spiwack <arnaud@spiwack.net>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16993 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'bootstrap')
| -rw-r--r-- | bootstrap/Monads.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v index 4c800d48c..2aceb9fbc 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. |