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

2 files changed, 12 insertions, 49 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.
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 95609e12d6..c88029921f 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -227,13 +227,8 @@ module Logical =
     (); (fun s e _ sk fk ->
       Obj.magic x s e __ (fun a fk0 ->
         let x0,c = a in
-        let sk0 = fun a0 fk1 ->
-          let y,c' = a0 in
-          sk (y,(if c then c' else false))
-            fk1
-        in
-        let a0,s0 = x0 in
-        sk0 (((),s0),true) fk0) fk)
+        let a0,s0 = x0 in sk (((),s0),c) fk0)
+        fk)
   
   (** val seq :
       unit t -> 'a1 t -> proofview ->
@@ -343,47 +338,15 @@ module Logical =
           (fun e0 ->
           IOBase.ret (Util.Inr e0)))
         (fun x0 ->
-        let sk0 = fun a fk0 ->
-          let sk0 = fun a0 fk1 ->
-            let x1,c = a0 in
-            let sk0 = fun a1 fk2 ->
-              let y,c' = a1 in
-              sk
-                (y,(if c then c' else false))
-                fk2
-            in
-            (match x1 with
-             | Util.Inl p ->
-               let p0,y = p in
-               let a1,s0 = p0 in
-               sk0 (((Util.Inl
-                 (a1,(fun e0 x2 ->
-                 y e0))),s0),true) fk1
-             | Util.Inr e0 ->
-               sk0 (((Util.Inr e0),s),true)
-                 fk1)
-          in
-          let x1,c = a in
-          let sk1 = fun a0 fk1 ->
-            let y,c' = a0 in
-            sk0 (y,(if c then c' else false))
-              fk1
-          in
-          (match x1 with
-           | Util.Inl p ->
-             let a0,y = p in
-             sk1 ((Util.Inl (a0,(fun e0 x2 ->
-               y e0))),true) fk0
-           | Util.Inr e0 ->
-             sk1 ((Util.Inr e0),true) fk0)
-        in
-        (match x0 with
-         | Util.Inl p ->
-           let p0,y = p in
-           let a,c = p0 in
-           sk0 ((Util.Inl (a,y)),c) fk
-         | Util.Inr e0 ->
-           sk0 ((Util.Inr e0),true) fk)))
+        match x0 with
+        | Util.Inl p ->
+          let p0,y = p in
+          let a,c = p0 in
+          let a0,s0 = a in
+          sk (((Util.Inl (a0,(fun e0 x1 x2 ->
+            y e0))),s0),c) fk
+        | Util.Inr e0 ->
+          sk (((Util.Inr e0),s),true) fk))
   
   (** val lift :
       'a1 NonLogical.t -> proofview ->