Fixing backtrace handling here and there.

2 files changed, 311 insertions, 565 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a0c64d29d..013b2f204 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -582,7 +582,9 @@ let tclTIMEOUT n t =
       end
       begin function
         | Proof_errors.Timeout -> Proofview_monad.NonLogical.ret (Util.Inr Timeout)
-        | Proof_errors.TacticFailure e -> Proofview_monad.NonLogical.ret (Util.Inr e)
+        | Proof_errors.TacticFailure e as src ->
+          let e = Backtrace.app_backtrace ~src ~dst:e in
+          Proofview_monad.NonLogical.ret (Util.Inr e)
         | e -> Proofview_monad.NonLogical.raise e
       end
   end >>= function
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 18f834910..90266c6d0 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -1,9 +1,6 @@
-(* This file has been generated by extraction
-   of bootstrap/Monad.v. It shouldn't be
-   modified directly. To regenerate it run
-   coqtop -batch -impredicative-set -l
-   bootstrap/Monad.v in Coq's source
-   directory. *)
+(* This file has been generated by extraction of bootstrap/Monads.v. It
+   shouldn't be modified directly. To regenerate it run coqtop -batch
+   -impredicative-set -l bootstrap/Monads.v in Coq's source directory. *)
 
 type __ = Obj.t
 let __ = let rec f _ = Obj.repr f in Obj.repr f
@@ -22,19 +19,15 @@ module IOBase =
   
   let ret = fun a -> (); fun () -> a
   
-  (** val bind :
-      'a1 coq_T -> ('a1 -> 'a2 coq_T) -> 'a2
-      coq_T **)
+  (** val bind : 'a1 coq_T -> ('a1 -> 'a2 coq_T) -> 'a2 coq_T **)
   
   let bind = fun a k -> (); fun () -> k (a ()) ()
   
-  (** val ignore :
-      'a1 coq_T -> unit coq_T **)
+  (** val ignore : 'a1 coq_T -> unit coq_T **)
   
   let ignore = fun a -> (); fun () -> ignore (a ())
   
-  (** val seq :
-      unit coq_T -> 'a1 coq_T -> 'a1 coq_T **)
+  (** val seq : unit coq_T -> 'a1 coq_T -> 'a1 coq_T **)
   
   let seq = fun a k -> (); fun () -> a (); k ()
   
@@ -42,8 +35,7 @@ module IOBase =
   
   let ref = fun a -> (); fun () -> Pervasives.ref a
   
-  (** val set :
-      'a1 coq_Ref -> 'a1 -> unit coq_T **)
+  (** val set : 'a1 coq_Ref -> 'a1 -> unit coq_T **)
   
   let set = fun r a -> (); fun () -> Pervasives.(:=) r a
   
@@ -55,27 +47,23 @@ module IOBase =
   
   let raise = fun e -> (); fun () -> raise (Proof_errors.Exception e)
   
-  (** val catch :
-      'a1 coq_T -> (exn -> 'a1 coq_T) -> 'a1
-      coq_T **)
+  (** val catch : 'a1 coq_T -> (exn -> 'a1 coq_T) -> 'a1 coq_T **)
   
-  let catch = fun s h -> (); fun () -> try s () with Proof_errors.Exception e -> h e ()
+  let catch = fun s h -> (); fun () -> try s () with Proof_errors.Exception e -> let e = Errors.push e in h e ()
   
   (** val read_line : string coq_T **)
   
-  let read_line = fun () -> try Pervasives.read_line () with e -> raise e ()
+  let read_line = fun () -> try Pervasives.read_line () with e -> let e = Errors.push e in raise e ()
   
   (** val print_char : char -> unit coq_T **)
   
   let print_char = fun c -> (); fun () -> print_char c
   
-  (** val print :
-      Pp.std_ppcmds -> unit coq_T **)
+  (** val print : Pp.std_ppcmds -> unit coq_T **)
   
-  let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> raise e ()
+  let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> let e = Errors.push e in raise e ()
   
-  (** val timeout :
-      int -> 'a1 coq_T -> 'a1 coq_T **)
+  (** val timeout : int -> 'a1 coq_T -> 'a1 coq_T **)
   
   let timeout = fun n t -> (); fun () ->
     let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
@@ -90,19 +78,19 @@ module IOBase =
       restore_timeout ();
       res
     with
-    | e -> restore_timeout (); Pervasives.raise e
+    | e ->
+      let e = Errors.push e in
+      restore_timeout ();
+      Pervasives.raise e
  
  end
 
-type proofview = { initial : (Term.constr*Term.types)
-                             list;
-                   solution : Evd.evar_map;
-                   comb : Goal.goal list }
+type proofview = { initial : (Term.constr*Term.types) list;
+                   solution : Evd.evar_map; comb : Goal.goal list }
 
 type logicalState = proofview
 
-type logicalMessageType =
-  bool*(Goal.goal list*Goal.goal list)
+type logicalMessageType = bool*(Goal.goal list*Goal.goal list)
 
 type logicalEnvironment = Environ.env
 
@@ -117,8 +105,7 @@ module NonLogical =
   let ret x =
     IOBase.ret x
   
-  (** val bind :
-      'a1 t -> ('a1 -> 'a2 t) -> 'a2 t **)
+  (** val bind : 'a1 t -> ('a1 -> 'a2 t) -> 'a2 t **)
   
   let bind x k =
     IOBase.bind x k
@@ -153,8 +140,7 @@ module NonLogical =
   let raise e =
     IOBase.raise e
   
-  (** val catch :
-      'a1 t -> (exn -> 'a1 t) -> 'a1 t **)
+  (** val catch : 'a1 t -> (exn -> 'a1 t) -> 'a1 t **)
   
   let catch s h =
     IOBase.catch s h
@@ -181,630 +167,388 @@ module NonLogical =
   
   (** val run : 'a1 t -> 'a1 **)
   
-  let run = fun x -> try x () with Proof_errors.Exception e -> Pervasives.raise e
+  let run = fun x -> try x () with Proof_errors.Exception e -> let e = Errors.push e in Pervasives.raise e
  end
 
 module Logical = 
  struct 
   type 'a t =
-    __ -> ('a -> 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) ->
-    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 -> __ ->
-    (__ -> __ -> (__ -> (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*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
+    __ -> ('a -> 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) -> 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 -> __ -> (__ -> __ -> (__ -> (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*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*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*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*Goal.goal list))
-      -> __ -> ('a4 -> (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
+      'a1 -> __ -> ('a1 -> proofview -> __ -> ('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*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*Goal.goal list)) ->
+      __ -> ('a4 -> (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 **)
   
   let ret x =
     (); (fun _ k s -> Obj.magic k x s)
   
   (** val bind :
-      'a1 t -> ('a1 -> 'a2 t) -> __ -> ('a2
-      -> proofview -> __ -> ('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 -> __ ->
-      (__ -> (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 -> __ ->
-      ('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*Goal.goal list))
-      -> __ -> ('a5 -> (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
+      'a1 t -> ('a1 -> 'a2 t) -> __ -> ('a2 -> proofview -> __ -> ('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 -> __ -> (__ -> (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 -> __ -> ('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*Goal.goal list)) ->
+      __ -> ('a5 -> (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 **)
   
   let bind x k =
-    (); (fun _ k0 s ->
-      Obj.magic x __ (fun a s' ->
-        Obj.magic k a __ k0 s') s)
+    (); (fun _ k0 s -> Obj.magic x __ (fun a s' -> Obj.magic k a __ k0 s') s)
   
   (** val ignore :
-      'a1 t -> __ -> (unit -> proofview -> __
-      -> ('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*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*Goal.goal list))
-      -> __ -> ('a4 -> (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
+      'a1 t -> __ -> (unit -> proofview -> __ -> ('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*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*Goal.goal list)) ->
+      __ -> ('a4 -> (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 **)
   
   let ignore x =
-    (); (fun _ k s ->
-      Obj.magic x __ (fun x1 s' -> k () s') s)
+    (); (fun _ k s -> Obj.magic x __ (fun x1 s' -> k () s') s)
   
   (** val seq :
-      unit t -> 'a1 t -> __ -> ('a1 ->
-      proofview -> __ -> ('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*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*Goal.goal list))
-      -> __ -> ('a4 -> (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
+      unit t -> 'a1 t -> __ -> ('a1 -> proofview -> __ -> ('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*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*Goal.goal list)) ->
+      __ -> ('a4 -> (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 **)
   
   let seq x k =
-    (); (fun _ k0 s ->
-      Obj.magic x __ (fun x1 s' ->
-        Obj.magic k __ k0 s') s)
+    (); (fun _ k0 s -> Obj.magic x __ (fun x1 s' -> Obj.magic k __ k0 s') s)
   
   (** val set :
-      logicalState -> __ -> (unit ->
-      proofview -> __ -> ('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*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 -> __ ->
-      ('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*Goal.goal list))
-      -> __ -> ('a3 -> (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
+      logicalState -> __ -> (unit -> proofview -> __ -> ('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*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 -> __ -> ('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*Goal.goal list)) ->
+      __ -> ('a3 -> (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 **)
   
   let set s =
     (); (fun _ k x -> Obj.magic k () s)
   
   (** val get :
-      __ -> (logicalState -> proofview -> __
-      -> ('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*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 -> __ ->
-      ('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*Goal.goal list))
-      -> __ -> ('a3 -> (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
+      __ -> (logicalState -> proofview -> __ -> ('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*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 -> __ -> ('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*Goal.goal list)) ->
+      __ -> ('a3 -> (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 **)
   
   let get r k s =
     Obj.magic k s s
   
   (** val put :
-      logicalMessageType -> __ -> (unit ->
-      proofview -> __ -> ('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*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 -> __ ->
-      ('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*Goal.goal list))
-      -> __ -> ('a3 -> (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
+      logicalMessageType -> __ -> (unit -> proofview -> __ -> ('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*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 -> __ -> ('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*Goal.goal list)) ->
+      __ -> ('a3 -> (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 **)
   
   let put m =
     (); (fun _ k s _ k0 e _ k1 ->
-      Obj.magic k () s __ k0 e __
-        (fun b c' ->
+      Obj.magic k () s __ k0 e __ (fun b c' ->
         k1 b
-          ((if fst m then fst c' else false),(
-          (List.append (fst (snd m))
-            (fst (snd c'))),(List.append
-                              (snd (snd m))
-                              (snd (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*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*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 -> __ ->
-      ('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*Goal.goal list))
-      -> __ -> ('a3 -> (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
+      __ -> (logicalEnvironment -> proofview -> __ -> ('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*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 -> __ -> ('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*Goal.goal list)) ->
+      __ -> ('a3 -> (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 **)
   
   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*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*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*Goal.goal list))
-      -> __ -> ('a4 -> (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
+      exn -> __ -> ('a1 -> proofview -> __ -> ('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*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*Goal.goal list)) ->
+      __ -> ('a4 -> (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 **)
   
   let zero e =
-    (); (fun _ k s _ k0 e0 _ k1 _ sk fk ->
-      fk e)
+    (); (fun _ k s _ k0 e0 _ k1 _ sk fk -> fk e)
   
   (** val plus :
-      'a1 t -> (exn -> 'a1 t) -> __ -> ('a1
-      -> proofview -> __ -> ('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*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*Goal.goal list))
-      -> __ -> ('a4 -> (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
+      'a1 t -> (exn -> 'a1 t) -> __ -> ('a1 -> proofview -> __ -> ('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*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*Goal.goal list)) ->
+      __ -> ('a4 -> (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 **)
   
   let plus x y =
     (); (fun _ k s _ k0 e _ k1 _ sk fk ->
-      Obj.magic x __ k s __ k0 e __ k1 __ sk
-        (fun e0 ->
-        Obj.magic y e0 __ k s __ k0 e __ k1
-          __ sk fk))
+      Obj.magic x __ k s __ k0 e __ k1 __ sk (fun e0 ->
+        Obj.magic y e0 __ k s __ k0 e __ k1 __ sk fk))
   
   (** val split :
-      'a1 t -> __ -> (('a1, exn -> 'a1 t)
-      list_view -> proofview -> __ -> ('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*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*Goal.goal list))
-      -> __ -> ('a4 -> (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
+      'a1 t -> __ -> (('a1, exn -> 'a1 t) list_view -> proofview -> __ ->
+      ('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*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*Goal.goal list)) ->
+      __ -> ('a4 -> (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 **)
   
   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 __
-          (fun a c _ sk0 fk0 ->
-          sk0 (a,c) fk0) __ (fun a fk0 ->
-          IOBase.ret (Cons (a,
-            (fun e0 _ sk0 fk1 ->
+        (Obj.magic x __ (fun a s' _ k2 e0 -> k2 (a,s')) s __ (fun a _ k2 ->
+          k2 a (true,([],[]))) e __ (fun a c _ sk0 fk0 -> sk0 (a,c) fk0) __
+          (fun a fk0 ->
+          IOBase.ret (Cons (a, (fun e0 _ sk0 fk1 ->
             IOBase.bind (fk0 e0) (fun x0 ->
               match x0 with
               | Nil e1 -> fk1 e1
-              | Cons (a0, x1) ->
-                sk0 a0 (fun e1 ->
-                  x1 e1 __ sk0 fk1))))))
-          (fun e0 -> IOBase.ret (Nil e0)))
-        (fun x0 ->
+              | Cons (a0, x1) -> sk0 a0 (fun e1 -> x1 e1 __ sk0 fk1))))))
+          (fun e0 -> IOBase.ret (Nil e0))) (fun x0 ->
         match x0 with
         | Nil exc ->
           let c = true,([],[]) in
-          Obj.magic k (Nil exc) s __ k0 e __
-            (fun b c' ->
+          Obj.magic k (Nil exc) s __ k0 e __ (fun b c' ->
             k1 b
-              ((if fst c
-                then fst c'
-                else false),((List.append
-                               (fst (snd c))
-                               (fst (snd c'))),
-              (List.append (snd (snd c))
-                (snd (snd c')))))) __ sk fk
+              ((if fst c then fst c' 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
-          Obj.magic k (Cons (a',
-            (fun exc _ k2 s0 _ k3 e0 _ k4 _ sk0 fk0 ->
+          Obj.magic k (Cons (a', (fun exc _ k2 s0 _ k3 e0 _ k4 _ sk0 fk0 ->
             y exc __ (fun a fk1 ->
               let a0,c = a in
               let a1,s'0 = a0 in
-              k2 a1 s'0 __ k3 e0 __
-                (fun b c' ->
+              k2 a1 s'0 __ k3 e0 __ (fun b c' ->
                 k4 b
-                  ((if fst c
-                    then fst 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' ->
+                  ((if fst c then fst 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
-                               (fst (snd m'))
-                               (fst (snd c'))),
-              (List.append (snd (snd m'))
-                (snd (snd c')))))) __ sk fk))
+              ((if fst m' then fst c' 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*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*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*Goal.goal list))
-      -> __ -> ('a4 -> (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
+      'a1 NonLogical.t -> __ -> ('a1 -> proofview -> __ -> ('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*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*Goal.goal list)) ->
+      __ -> ('a4 -> (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 **)
   
   let lift x =
     (); (fun _ k s _ k0 e _ k1 _ sk fk ->
       IOBase.bind x (fun x0 ->
-        Obj.magic k x0 s __ k0 e __
-          (fun b c' ->
+        Obj.magic k x0 s __ k0 e __ (fun b c' ->
           k1 b
-            ((if fst (true,([],[]))
-              then fst c'
-              else false),((List.append
-                             (fst
-                               (snd
-                                 (true,([],[]))))
-                             (fst (snd c'))),
-            (List.append
-              (snd (snd (true,([],[]))))
-              (snd (snd c')))))) __ sk fk))
+            ((if fst (true,([],[])) then fst c' 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 ->
-      logicalState ->
-      (('a1*logicalState)*logicalMessageType)
-      NonLogical.t **)
+      'a1 t -> logicalEnvironment -> logicalState ->
+      (('a1*logicalState)*logicalMessageType) NonLogical.t **)
   
   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) __
+    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 ->
-      IOBase.raise
-        ((fun e -> Proof_errors.TacticFailure e)
-          e0))
+      IOBase.raise ((fun e -> Proof_errors.TacticFailure e) e0))
  end