diff options
| -rw-r--r-- | bootstrap/Monads.v | 2 | ||||
| -rw-r--r-- | proofs/proofview_gen.ml | 59 |
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 -> |