diff options
Diffstat (limited to 'proofs/proofview_gen.ml')
| -rw-r--r-- | proofs/proofview_gen.ml | 56 |
1 files changed, 28 insertions, 28 deletions
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml index ad87b7328..d168188de 100644 --- a/proofs/proofview_gen.ml +++ b/proofs/proofview_gen.ml @@ -8,6 +8,10 @@ type __ = Obj.t let __ = let rec f _ = Obj.repr f in Obj.repr f +type ('a, 'b) list_view = +| Nil of exn +| Cons of 'a * 'b + module IOBase = struct type 'a coq_T = unit -> 'a @@ -354,17 +358,16 @@ module Logical = Obj.magic y e __ k s env __ sk fk)) (** val split : - 'a1 t -> __ -> (('a1*(exn -> 'a1 t), - exn) Util.union -> proofview -> - Environ.env -> __ -> (('a2*bool) -> - (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ + 'a1 t -> __ -> (('a1, exn -> 'a1 t) + list_view -> proofview -> Environ.env + -> __ -> (('a2*bool) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - proofview -> Environ.env -> __ -> - (('a2*bool) -> (exn -> 'a3 - IOBase.coq_T) -> 'a3 IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> proofview -> + Environ.env -> __ -> (('a2*bool) -> (exn -> 'a3 IOBase.coq_T) -> 'a3 - IOBase.coq_T **) + IOBase.coq_T) -> (exn -> 'a3 + IOBase.coq_T) -> 'a3 IOBase.coq_T **) let split x = (); (fun _ k s e _ sk fk -> @@ -373,25 +376,26 @@ module Logical = (fun a s' e0 _ sk0 fk0 -> sk0 ((a,s'),true) fk0) s e __ (fun a fk0 -> - IOBase.ret (Util.Inl - (a,(fun e0 _ sk0 fk1 -> + IOBase.ret (Cons (a, + (fun e0 _ sk0 fk1 -> IOBase.bind (fk0 e0) (fun x0 -> match x0 with - | Util.Inl p -> - let a0,x1 = p in + | Nil e1 -> fk1 e1 + | Cons (a0, x1) -> sk0 a0 (fun e1 -> - x1 e1 __ sk0 fk1) - | Util.Inr e1 -> fk1 e1))))) - (fun e0 -> - IOBase.ret (Util.Inr e0))) + x1 e1 __ sk0 fk1)))))) + (fun e0 -> IOBase.ret (Nil e0))) (fun x0 -> match x0 with - | Util.Inl p -> - let p0,y = p in - let p1,m' = p0 in - let a',s' = p1 in - Obj.magic k (Util.Inl - (a',(fun exc _ k0 s0 e0 _ sk0 fk0 -> + | Nil exc -> + Obj.magic k (Nil exc) s e __ + (fun a fk0 -> + let y,c' = a in sk (y,c') fk0) fk + | Cons (p, y) -> + let p0,m' = p in + let a',s' = p0 in + Obj.magic k (Cons (a', + (fun exc _ k0 s0 e0 _ sk0 fk0 -> y exc __ (fun a fk1 -> let x1,c = a in let a0,s'0 = x1 in @@ -405,11 +409,7 @@ module Logical = let y0,c' = a in sk (y0,(if m' then c' else false)) - fk0) fk - | Util.Inr exc -> - Obj.magic k (Util.Inr exc) s e __ - (fun a fk0 -> - let y,c' = a in sk (y,c') fk0) fk)) + fk0) fk)) (** val lift : 'a1 NonLogical.t -> __ -> ('a1 -> |