diff options
Diffstat (limited to 'proofs/proofview_gen.ml')
| -rw-r--r-- | proofs/proofview_gen.ml | 603 |
1 files changed, 324 insertions, 279 deletions
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml index b813eabaa..18f834910 100644 --- a/proofs/proofview_gen.ml +++ b/proofs/proofview_gen.ml @@ -101,7 +101,8 @@ type proofview = { initial : (Term.constr*Term.types) type logicalState = proofview -type logicalMessageType = bool*Goal.goal list +type logicalMessageType = + bool*(Goal.goal list*Goal.goal list) type logicalEnvironment = Environ.env @@ -187,68 +188,73 @@ module Logical = struct type 'a t = __ -> ('a -> proofview -> __ -> (__ -> __ - -> (__ -> (bool*Goal.goal list) -> __ -> - (__ -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ IOBase.coq_T) - -> __ IOBase.coq_T) -> __ -> (__ -> (exn - -> __ IOBase.coq_T) -> __ IOBase.coq_T) - -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> Environ.env -> __ -> (__ - -> (bool*Goal.goal list) -> __ -> (__ -> - (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ IOBase.coq_T) - -> __ IOBase.coq_T) -> __ -> (__ -> (exn + -> (__ -> (bool*(Goal.goal list*Goal.goal + list)) -> __ -> (__ -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) - -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> proofview -> __ -> (__ - -> __ -> (__ -> (bool*Goal.goal list) -> + -> __ -> (__ -> (exn -> __ IOBase.coq_T) + -> __ IOBase.coq_T) -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> + Environ.env -> __ -> (__ -> + (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) - -> __ IOBase.coq_T) -> Environ.env -> __ - -> (__ -> (bool*Goal.goal list) -> __ -> - (__ -> (exn -> __ IOBase.coq_T) -> __ + -> __ IOBase.coq_T) -> proofview -> __ -> + (__ -> __ -> (__ -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> + (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T + IOBase.coq_T) -> Environ.env -> __ -> (__ + -> (bool*(Goal.goal list*Goal.goal list)) + -> __ -> (__ -> (exn -> __ IOBase.coq_T) + -> __ IOBase.coq_T) -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> __ + -> (__ -> (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> (exn -> __ IOBase.coq_T) + -> __ IOBase.coq_T (** val ret : 'a1 -> __ -> ('a1 -> proofview -> __ -> - ('a2 -> __ -> (__ -> (bool*Goal.goal - list) -> __ -> (__ -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> + ('a2 -> __ -> (__ -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> __ -> (__ -> (exn -> - __ IOBase.coq_T) -> __ IOBase.coq_T) -> - (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> Environ.env -> __ -> - (__ -> (bool*Goal.goal list) -> __ -> - (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - proofview -> __ -> ('a2 -> __ -> ('a3 - -> (bool*Goal.goal list) -> __ -> (__ - -> (exn -> __ IOBase.coq_T) -> __ + Environ.env -> __ -> (__ -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> (__ -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> proofview -> __ -> + ('a2 -> __ -> ('a3 -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> + (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> ('a3 -> - (bool*Goal.goal list) -> __ -> ('a4 -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> ('a4 -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> ('a4 -> (exn -> 'a5 IOBase.coq_T) -> - 'a5 IOBase.coq_T) -> (exn -> 'a5 - IOBase.coq_T) -> 'a5 IOBase.coq_T **) + IOBase.coq_T) -> __ -> ('a4 -> (exn -> + 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T) + -> (exn -> 'a5 IOBase.coq_T) -> 'a5 + IOBase.coq_T **) let ret x = (); (fun _ k s -> Obj.magic k x s) @@ -256,37 +262,39 @@ module Logical = (** val bind : 'a1 t -> ('a1 -> 'a2 t) -> __ -> ('a2 -> proofview -> __ -> ('a3 -> __ -> (__ - -> (bool*Goal.goal list) -> __ -> (__ - -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + -> (bool*(Goal.goal list*Goal.goal + list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - Environ.env -> __ -> (__ -> - (bool*Goal.goal list) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> Environ.env -> __ -> + (__ -> (bool*(Goal.goal list*Goal.goal + list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - proofview -> __ -> ('a3 -> __ -> ('a4 - -> (bool*Goal.goal list) -> __ -> (__ - -> (exn -> __ IOBase.coq_T) -> __ + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> proofview -> __ -> + ('a3 -> __ -> ('a4 -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> + (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> ('a4 -> - (bool*Goal.goal list) -> __ -> ('a5 -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> ('a5 -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> ('a5 -> (exn -> 'a6 IOBase.coq_T) -> - 'a6 IOBase.coq_T) -> (exn -> 'a6 - IOBase.coq_T) -> 'a6 IOBase.coq_T **) + IOBase.coq_T) -> __ -> ('a5 -> (exn -> + 'a6 IOBase.coq_T) -> 'a6 IOBase.coq_T) + -> (exn -> 'a6 IOBase.coq_T) -> 'a6 + IOBase.coq_T **) let bind x k = (); (fun _ k0 s -> @@ -295,37 +303,40 @@ module Logical = (** val ignore : 'a1 t -> __ -> (unit -> proofview -> __ - -> ('a2 -> __ -> (__ -> (bool*Goal.goal - list) -> __ -> (__ -> (exn -> __ + -> ('a2 -> __ -> (__ -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> - (__ -> (bool*Goal.goal list) -> __ -> - (__ -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + (__ -> (bool*(Goal.goal list*Goal.goal + list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - proofview -> __ -> ('a2 -> __ -> ('a3 - -> (bool*Goal.goal list) -> __ -> (__ - -> (exn -> __ IOBase.coq_T) -> __ + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> proofview -> __ -> + ('a2 -> __ -> ('a3 -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> + (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> ('a3 -> - (bool*Goal.goal list) -> __ -> ('a4 -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> ('a4 -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> ('a4 -> (exn -> 'a5 IOBase.coq_T) -> - 'a5 IOBase.coq_T) -> (exn -> 'a5 - IOBase.coq_T) -> 'a5 IOBase.coq_T **) + IOBase.coq_T) -> __ -> ('a4 -> (exn -> + 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T) + -> (exn -> 'a5 IOBase.coq_T) -> 'a5 + IOBase.coq_T **) let ignore x = (); (fun _ k s -> @@ -334,37 +345,39 @@ module Logical = (** val seq : unit t -> 'a1 t -> __ -> ('a1 -> proofview -> __ -> ('a2 -> __ -> (__ -> - (bool*Goal.goal list) -> __ -> (__ -> - (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - Environ.env -> __ -> (__ -> - (bool*Goal.goal list) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> Environ.env -> __ -> + (__ -> (bool*(Goal.goal list*Goal.goal + list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - proofview -> __ -> ('a2 -> __ -> ('a3 - -> (bool*Goal.goal list) -> __ -> (__ - -> (exn -> __ IOBase.coq_T) -> __ + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> proofview -> __ -> + ('a2 -> __ -> ('a3 -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> + (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> ('a3 -> - (bool*Goal.goal list) -> __ -> ('a4 -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> ('a4 -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> ('a4 -> (exn -> 'a5 IOBase.coq_T) -> - 'a5 IOBase.coq_T) -> (exn -> 'a5 - IOBase.coq_T) -> 'a5 IOBase.coq_T **) + IOBase.coq_T) -> __ -> ('a4 -> (exn -> + 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T) + -> (exn -> 'a5 IOBase.coq_T) -> 'a5 + IOBase.coq_T **) let seq x k = (); (fun _ k0 s -> @@ -374,74 +387,79 @@ module Logical = (** val set : logicalState -> __ -> (unit -> proofview -> __ -> ('a1 -> __ -> (__ -> - (bool*Goal.goal list) -> __ -> (__ -> - (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - Environ.env -> __ -> (__ -> - (bool*Goal.goal list) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> Environ.env -> __ -> + (__ -> (bool*(Goal.goal list*Goal.goal + list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - proofview -> __ -> ('a1 -> __ -> ('a2 - -> (bool*Goal.goal list) -> __ -> (__ - -> (exn -> __ IOBase.coq_T) -> __ + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> proofview -> __ -> + ('a1 -> __ -> ('a2 -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> + (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> ('a2 -> - (bool*Goal.goal list) -> __ -> ('a3 -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> ('a3 -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> ('a3 -> (exn -> 'a4 IOBase.coq_T) -> - 'a4 IOBase.coq_T) -> (exn -> 'a4 - IOBase.coq_T) -> 'a4 IOBase.coq_T **) + IOBase.coq_T) -> __ -> ('a3 -> (exn -> + 'a4 IOBase.coq_T) -> 'a4 IOBase.coq_T) + -> (exn -> 'a4 IOBase.coq_T) -> 'a4 + IOBase.coq_T **) let set s = (); (fun _ k x -> Obj.magic k () s) (** val get : __ -> (logicalState -> proofview -> __ - -> ('a1 -> __ -> (__ -> (bool*Goal.goal - list) -> __ -> (__ -> (exn -> __ + -> ('a1 -> __ -> (__ -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> - (__ -> (bool*Goal.goal list) -> __ -> - (__ -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + (__ -> (bool*(Goal.goal list*Goal.goal + list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - proofview -> __ -> ('a1 -> __ -> ('a2 - -> (bool*Goal.goal list) -> __ -> (__ - -> (exn -> __ IOBase.coq_T) -> __ + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> proofview -> __ -> + ('a1 -> __ -> ('a2 -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> + (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> ('a2 -> - (bool*Goal.goal list) -> __ -> ('a3 -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> ('a3 -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> ('a3 -> (exn -> 'a4 IOBase.coq_T) -> - 'a4 IOBase.coq_T) -> (exn -> 'a4 - IOBase.coq_T) -> 'a4 IOBase.coq_T **) + IOBase.coq_T) -> __ -> ('a3 -> (exn -> + 'a4 IOBase.coq_T) -> 'a4 IOBase.coq_T) + -> (exn -> 'a4 IOBase.coq_T) -> 'a4 + IOBase.coq_T **) let get r k s = Obj.magic k s s @@ -449,117 +467,127 @@ module Logical = (** val put : logicalMessageType -> __ -> (unit -> proofview -> __ -> ('a1 -> __ -> (__ -> - (bool*Goal.goal list) -> __ -> (__ -> - (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - Environ.env -> __ -> (__ -> - (bool*Goal.goal list) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> Environ.env -> __ -> + (__ -> (bool*(Goal.goal list*Goal.goal + list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - proofview -> __ -> ('a1 -> __ -> ('a2 - -> (bool*Goal.goal list) -> __ -> (__ - -> (exn -> __ IOBase.coq_T) -> __ + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> proofview -> __ -> + ('a1 -> __ -> ('a2 -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> + (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> ('a2 -> - (bool*Goal.goal list) -> __ -> ('a3 -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> ('a3 -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> ('a3 -> (exn -> 'a4 IOBase.coq_T) -> - 'a4 IOBase.coq_T) -> (exn -> 'a4 - IOBase.coq_T) -> 'a4 IOBase.coq_T **) + IOBase.coq_T) -> __ -> ('a3 -> (exn -> + 'a4 IOBase.coq_T) -> 'a4 IOBase.coq_T) + -> (exn -> 'a4 IOBase.coq_T) -> 'a4 + IOBase.coq_T **) let put m = (); (fun _ k s _ k0 e _ k1 -> Obj.magic k () s __ k0 e __ (fun b c' -> k1 b - ((if fst m then fst c' else false), - (List.append (snd m) (snd c'))))) + ((if fst m then fst c' else false),( + (List.append (fst (snd m)) + (fst (snd c'))),(List.append + (snd (snd m)) + (snd (snd c'))))))) (** val current : __ -> (logicalEnvironment -> proofview -> __ -> ('a1 -> __ -> (__ -> - (bool*Goal.goal list) -> __ -> (__ -> - (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - Environ.env -> __ -> (__ -> - (bool*Goal.goal list) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> Environ.env -> __ -> + (__ -> (bool*(Goal.goal list*Goal.goal + list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - proofview -> __ -> ('a1 -> __ -> ('a2 - -> (bool*Goal.goal list) -> __ -> (__ - -> (exn -> __ IOBase.coq_T) -> __ + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> proofview -> __ -> + ('a1 -> __ -> ('a2 -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> + (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> ('a2 -> - (bool*Goal.goal list) -> __ -> ('a3 -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> ('a3 -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> ('a3 -> (exn -> 'a4 IOBase.coq_T) -> - 'a4 IOBase.coq_T) -> (exn -> 'a4 - IOBase.coq_T) -> 'a4 IOBase.coq_T **) + IOBase.coq_T) -> __ -> ('a3 -> (exn -> + 'a4 IOBase.coq_T) -> 'a4 IOBase.coq_T) + -> (exn -> 'a4 IOBase.coq_T) -> 'a4 + IOBase.coq_T **) let current r k s r0 k0 e = Obj.magic k e s __ k0 e (** val zero : exn -> __ -> ('a1 -> proofview -> __ -> - ('a2 -> __ -> (__ -> (bool*Goal.goal - list) -> __ -> (__ -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> + ('a2 -> __ -> (__ -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> __ -> (__ -> (exn -> - __ IOBase.coq_T) -> __ IOBase.coq_T) -> - (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> Environ.env -> __ -> - (__ -> (bool*Goal.goal list) -> __ -> - (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - proofview -> __ -> ('a2 -> __ -> ('a3 - -> (bool*Goal.goal list) -> __ -> (__ - -> (exn -> __ IOBase.coq_T) -> __ + Environ.env -> __ -> (__ -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> (__ -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> proofview -> __ -> + ('a2 -> __ -> ('a3 -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> + (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> ('a3 -> - (bool*Goal.goal list) -> __ -> ('a4 -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> ('a4 -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> ('a4 -> (exn -> 'a5 IOBase.coq_T) -> - 'a5 IOBase.coq_T) -> (exn -> 'a5 - IOBase.coq_T) -> 'a5 IOBase.coq_T **) + IOBase.coq_T) -> __ -> ('a4 -> (exn -> + 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T) + -> (exn -> 'a5 IOBase.coq_T) -> 'a5 + IOBase.coq_T **) let zero e = (); (fun _ k s _ k0 e0 _ k1 _ sk fk -> @@ -568,37 +596,39 @@ module Logical = (** val plus : 'a1 t -> (exn -> 'a1 t) -> __ -> ('a1 -> proofview -> __ -> ('a2 -> __ -> (__ - -> (bool*Goal.goal list) -> __ -> (__ - -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + -> (bool*(Goal.goal list*Goal.goal + list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - Environ.env -> __ -> (__ -> - (bool*Goal.goal list) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> Environ.env -> __ -> + (__ -> (bool*(Goal.goal list*Goal.goal + list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - proofview -> __ -> ('a2 -> __ -> ('a3 - -> (bool*Goal.goal list) -> __ -> (__ - -> (exn -> __ IOBase.coq_T) -> __ + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> proofview -> __ -> + ('a2 -> __ -> ('a3 -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> + (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> ('a3 -> - (bool*Goal.goal list) -> __ -> ('a4 -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> ('a4 -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> ('a4 -> (exn -> 'a5 IOBase.coq_T) -> - 'a5 IOBase.coq_T) -> (exn -> 'a5 - IOBase.coq_T) -> 'a5 IOBase.coq_T **) + IOBase.coq_T) -> __ -> ('a4 -> (exn -> + 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T) + -> (exn -> 'a5 IOBase.coq_T) -> 'a5 + IOBase.coq_T **) let plus x y = (); (fun _ k s _ k0 e _ k1 _ sk fk -> @@ -610,44 +640,47 @@ module Logical = (** val split : 'a1 t -> __ -> (('a1, exn -> 'a1 t) list_view -> proofview -> __ -> ('a2 -> - __ -> (__ -> (bool*Goal.goal list) -> - __ -> (__ -> (exn -> __ IOBase.coq_T) - -> __ IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> - Environ.env -> __ -> (__ -> - (bool*Goal.goal list) -> __ -> (__ -> + __ -> (__ -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - proofview -> __ -> ('a2 -> __ -> ('a3 - -> (bool*Goal.goal list) -> __ -> (__ - -> (exn -> __ IOBase.coq_T) -> __ + Environ.env -> __ -> (__ -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> (__ -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> proofview -> __ -> + ('a2 -> __ -> ('a3 -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> + (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> ('a3 -> - (bool*Goal.goal list) -> __ -> ('a4 -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> ('a4 -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> ('a4 -> (exn -> 'a5 IOBase.coq_T) -> - 'a5 IOBase.coq_T) -> (exn -> 'a5 - IOBase.coq_T) -> 'a5 IOBase.coq_T **) + IOBase.coq_T) -> __ -> ('a4 -> (exn -> + 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T) + -> (exn -> 'a5 IOBase.coq_T) -> 'a5 + IOBase.coq_T **) let split x = (); (fun _ k s _ k0 e _ k1 _ sk fk -> IOBase.bind (Obj.magic x __ (fun a s' _ k2 e0 -> k2 (a,s')) s __ (fun a _ k2 -> - k2 a (true,[])) e __ + k2 a (true,([],[]))) e __ (fun a c _ sk0 fk0 -> sk0 (a,c) fk0) __ (fun a fk0 -> IOBase.ret (Cons (a, @@ -662,16 +695,17 @@ module Logical = (fun x0 -> match x0 with | Nil exc -> - let c = true,[] in + let c = true,([],[]) in Obj.magic k (Nil exc) s __ k0 e __ (fun b c' -> k1 b ((if fst c then fst c' - else false),(List.append - (snd c) - (snd c')))) __ - sk fk + else false),((List.append + (fst (snd c)) + (fst (snd c'))), + (List.append (snd (snd c)) + (snd (snd c')))))) __ sk fk | Cons (p, y) -> let p0,m' = p in let a',s' = p0 in @@ -685,53 +719,60 @@ module Logical = k4 b ((if fst c then fst c' - else false),(List.append - (snd c) - (snd c')))) - __ sk0 fk1) fk0))) s' __ k0 e - __ (fun b c' -> + else false),((List.append + (fst + (snd c)) + (fst + (snd c'))), + (List.append (snd (snd c)) + (snd (snd c')))))) __ sk0 + fk1) fk0))) s' __ k0 e __ + (fun b c' -> k1 b ((if fst m' then fst c' - else false),(List.append - (snd m') - (snd c')))) __ - sk fk)) + else false),((List.append + (fst (snd m')) + (fst (snd c'))), + (List.append (snd (snd m')) + (snd (snd c')))))) __ sk fk)) (** val lift : 'a1 NonLogical.t -> __ -> ('a1 -> proofview -> __ -> ('a2 -> __ -> (__ -> - (bool*Goal.goal list) -> __ -> (__ -> - (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - Environ.env -> __ -> (__ -> - (bool*Goal.goal list) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> (__ -> (exn -> __ IOBase.coq_T) -> - __ IOBase.coq_T) -> (exn -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> Environ.env -> __ -> + (__ -> (bool*(Goal.goal list*Goal.goal + list)) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> - proofview -> __ -> ('a2 -> __ -> ('a3 - -> (bool*Goal.goal list) -> __ -> (__ - -> (exn -> __ IOBase.coq_T) -> __ + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> __ -> (__ -> (exn -> + __ IOBase.coq_T) -> __ IOBase.coq_T) -> + (exn -> __ IOBase.coq_T) -> __ + IOBase.coq_T) -> proofview -> __ -> + ('a2 -> __ -> ('a3 -> (bool*(Goal.goal + list*Goal.goal list)) -> __ -> (__ -> + (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> Environ.env -> __ -> ('a3 -> - (bool*Goal.goal list) -> __ -> ('a4 -> + (bool*(Goal.goal list*Goal.goal list)) + -> __ -> ('a4 -> (exn -> __ + IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ - IOBase.coq_T) -> (exn -> __ - IOBase.coq_T) -> __ IOBase.coq_T) -> __ - -> ('a4 -> (exn -> 'a5 IOBase.coq_T) -> - 'a5 IOBase.coq_T) -> (exn -> 'a5 - IOBase.coq_T) -> 'a5 IOBase.coq_T **) + IOBase.coq_T) -> __ -> ('a4 -> (exn -> + 'a5 IOBase.coq_T) -> 'a5 IOBase.coq_T) + -> (exn -> 'a5 IOBase.coq_T) -> 'a5 + IOBase.coq_T **) let lift x = (); (fun _ k s _ k0 e _ k1 _ sk fk -> @@ -739,12 +780,16 @@ module Logical = Obj.magic k x0 s __ k0 e __ (fun b c' -> k1 b - ((if fst (true,[]) + ((if fst (true,([],[])) then fst c' - else false),(List.append - (snd (true,[])) - (snd c')))) __ sk - fk)) + else false),((List.append + (fst + (snd + (true,([],[])))) + (fst (snd c'))), + (List.append + (snd (snd (true,([],[])))) + (snd (snd c')))))) __ sk fk)) (** val run : 'a1 t -> logicalEnvironment -> @@ -755,9 +800,9 @@ module Logical = let run x e s = Obj.magic x __ (fun a s' _ k e0 -> k (a,s')) s __ (fun a _ k -> - k a (true,[])) e __ (fun a c _ sk fk -> - sk (a,c) fk) __ (fun a x0 -> - IOBase.ret a) (fun e0 -> + k a (true,([],[]))) e __ + (fun a c _ sk fk -> sk (a,c) fk) __ + (fun a x0 -> IOBase.ret a) (fun e0 -> IOBase.raise ((fun e -> Proof_errors.TacticFailure e) e0)) |