aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proofview_gen.ml208
1 files changed, 110 insertions, 98 deletions
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 422095870..95609e12d 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -1,7 +1,7 @@
(* 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
+ coqtop -batch -impredicative-set -l
bootstrap/Monad.v in Coq's source
directory. *)
@@ -16,46 +16,46 @@ module IOBase =
(** val ret : 'a1 -> 'a1 coq_T **)
- let ret = fun a () -> a
+ let ret = fun a -> (); fun () -> a
(** val bind :
'a1 coq_T -> ('a1 -> 'a2 coq_T) -> 'a2
coq_T **)
- let bind = fun a k () -> k (a ()) ()
+ let bind = fun a k -> (); fun () -> k (a ()) ()
(** val ignore :
'a1 coq_T -> unit coq_T **)
- let ignore = fun a () -> ignore (a ())
+ let ignore = fun a -> (); fun () -> ignore (a ())
(** val seq :
unit coq_T -> 'a1 coq_T -> 'a1 coq_T **)
- let seq = fun a k () -> a (); k ()
+ let seq = fun a k -> (); fun () -> a (); k ()
(** val ref : 'a1 -> 'a1 coq_Ref coq_T **)
- let ref = fun a () -> Pervasives.ref a
+ let ref = fun a -> (); fun () -> Pervasives.ref a
(** val set :
'a1 coq_Ref -> 'a1 -> unit coq_T **)
- let set = fun r a () -> Pervasives.(:=) r a
+ let set = fun r a -> (); fun () -> Pervasives.(:=) r a
(** val get : 'a1 coq_Ref -> 'a1 coq_T **)
- let get = fun r () -> Pervasives.(!) r
+ let get = fun r -> (); fun () -> Pervasives.(!) r
(** val raise : exn -> 'a1 coq_T **)
- let raise = fun e () -> raise (Proof_errors.Exception e)
+ let raise = fun e -> (); fun () -> raise (Proof_errors.Exception e)
(** val catch :
'a1 coq_T -> (exn -> 'a1 coq_T) -> 'a1
coq_T **)
- let catch = fun s h () -> try s () with Proof_errors.Exception e -> h e ()
+ let catch = fun s h -> (); fun () -> try s () with Proof_errors.Exception e -> h e ()
(** val read_line : string coq_T **)
@@ -63,17 +63,17 @@ module IOBase =
(** val print_char : char -> unit coq_T **)
- let print_char = fun c () -> print_char c
+ let print_char = fun c -> (); fun () -> print_char c
(** val print :
Pp.std_ppcmds -> unit coq_T **)
- let print = fun s () -> 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 -> raise e ()
(** val timeout :
int -> 'a1 coq_T -> 'a1 coq_T **)
- let timeout = fun n t () ->
+ let timeout = fun n t -> (); fun () ->
let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
Pervasives.ignore (Unix.alarm n);
@@ -194,8 +194,9 @@ module Logical =
-> (exn -> 'a2 IOBase.coq_T) -> 'a2
IOBase.coq_T **)
- let ret x s e r sk fk =
- sk ((x,s),true) fk
+ let ret x =
+ (); (fun s e _ sk fk ->
+ sk ((x,s),true) fk)
(** val bind :
'a1 t -> ('a1 -> 'a2 t) -> proofview ->
@@ -205,14 +206,15 @@ module Logical =
(exn -> 'a3 IOBase.coq_T) -> 'a3
IOBase.coq_T **)
- let bind x k s e r sk fk =
- Obj.magic x s e __ (fun a fk0 ->
- let x0,c = a in
- let x1,s0 = x0 in
- Obj.magic k x1 s0 e __ (fun a0 fk1 ->
- let y,c' = a0 in
- sk (y,(if c then c' else false)) fk1)
- fk0) fk
+ let bind x k =
+ (); (fun s e _ sk fk ->
+ Obj.magic x s e __ (fun a fk0 ->
+ let x0,c = a in
+ let x1,s0 = x0 in
+ Obj.magic k x1 s0 e __ (fun a0 fk1 ->
+ let y,c' = a0 in
+ sk (y,(if c then c' else false))
+ fk1) fk0) fk)
(** val ignore :
'a1 t -> proofview -> Environ.env -> __
@@ -221,15 +223,17 @@ module Logical =
-> (exn -> 'a2 IOBase.coq_T) -> 'a2
IOBase.coq_T **)
- let ignore x s e r 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 ignore x =
+ (); (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)
(** val seq :
unit t -> 'a1 t -> proofview ->
@@ -239,14 +243,15 @@ module Logical =
(exn -> 'a2 IOBase.coq_T) -> 'a2
IOBase.coq_T **)
- let seq x k s e r sk fk =
- Obj.magic x s e __ (fun a fk0 ->
- let x0,c = a in
- let u,s0 = x0 in
- Obj.magic k s0 e __ (fun a0 fk1 ->
- let y,c' = a0 in
- sk (y,(if c then c' else false)) fk1)
- fk0) fk
+ let seq x k =
+ (); (fun s e _ sk fk ->
+ Obj.magic x s e __ (fun a fk0 ->
+ let x0,c = a in
+ let u,s0 = x0 in
+ Obj.magic k s0 e __ (fun a0 fk1 ->
+ let y,c' = a0 in
+ sk (y,(if c then c' else false))
+ fk1) fk0) fk)
(** val set :
logicalState -> proofview ->
@@ -256,8 +261,9 @@ module Logical =
(exn -> 'a1 IOBase.coq_T) -> 'a1
IOBase.coq_T **)
- let set s s0 e r sk fk =
- sk (((),s),true) fk
+ let set s =
+ (); (fun s0 e _ sk fk ->
+ sk (((),s),true) fk)
(** val get :
proofview -> Environ.env -> __ ->
@@ -277,8 +283,8 @@ module Logical =
(exn -> 'a1 IOBase.coq_T) -> 'a1
IOBase.coq_T **)
- let put m s e r sk fk =
- sk (((),s),m) fk
+ let put m =
+ (); (fun s e _ sk fk -> sk (((),s),m) fk)
(** val current :
proofview -> Environ.env -> __ ->
@@ -297,8 +303,8 @@ module Logical =
-> (exn -> 'a2 IOBase.coq_T) -> 'a2
IOBase.coq_T **)
- let zero e s e0 r sk fk =
- fk e
+ let zero e =
+ (); (fun s e0 _ sk fk -> fk e)
(** val plus :
'a1 t -> (exn -> 'a1 t) -> proofview ->
@@ -308,9 +314,10 @@ module Logical =
(exn -> 'a2 IOBase.coq_T) -> 'a2
IOBase.coq_T **)
- let plus x y s env r sk fk =
- Obj.magic x s env __ sk (fun e ->
- Obj.magic y e s env __ sk fk)
+ let plus x y =
+ (); (fun s env _ sk fk ->
+ Obj.magic x s env __ sk (fun e ->
+ Obj.magic y e s env __ sk fk))
(** val split :
'a1 t -> proofview -> Environ.env -> __
@@ -320,59 +327,63 @@ module Logical =
-> (exn -> 'a2 IOBase.coq_T) -> 'a2
IOBase.coq_T **)
- let split x s e r sk fk =
- IOBase.bind
- (Obj.magic x s e __ (fun a fk0 ->
- IOBase.ret (Util.Inl
- (a,(fun e0 _ sk0 fk1 ->
- IOBase.bind (fk0 e0) (fun x0 ->
- match x0 with
- | Util.Inl p ->
- let a0,x1 = p in
- sk0 a0 (fun e1 ->
- x1 e1 __ sk0 fk1)
- | Util.Inr e1 -> fk1 e1)))))
- (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
+ let split x =
+ (); (fun s e _ sk fk ->
+ IOBase.bind
+ (Obj.magic x s e __ (fun a fk0 ->
+ IOBase.ret (Util.Inl
+ (a,(fun e0 _ sk0 fk1 ->
+ IOBase.bind (fk0 e0) (fun x0 ->
+ match x0 with
+ | Util.Inl p ->
+ let a0,x1 = p in
+ sk0 a0 (fun e1 ->
+ x1 e1 __ sk0 fk1)
+ | Util.Inr e1 -> fk1 e1)))))
+ (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 p0,y = p in
- let a1,s0 = p0 in
- sk0 (((Util.Inl
- (a1,(fun e0 x2 ->
- y e0))),s0),true) fk1
+ let a0,y = p in
+ sk1 ((Util.Inl (a0,(fun e0 x2 ->
+ y e0))),true) fk0
| 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
+ sk1 ((Util.Inr e0),true) fk0)
in
- (match x1 with
+ (match x0 with
| Util.Inl p ->
- let a0,y = p in
- sk1 ((Util.Inl (a0,(fun e0 x2 ->
- y e0))),true) fk0
+ let p0,y = p in
+ let a,c = p0 in
+ sk0 ((Util.Inl (a,y)),c) fk
| 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))
+ sk0 ((Util.Inr e0),true) fk)))
(** val lift :
'a1 NonLogical.t -> proofview ->
@@ -382,9 +393,10 @@ module Logical =
(exn -> 'a2 IOBase.coq_T) -> 'a2
IOBase.coq_T **)
- let lift x s e r sk fk =
- IOBase.bind x (fun x0 ->
- sk ((x0,s),true) fk)
+ let lift x =
+ (); (fun s e _ sk fk ->
+ IOBase.bind x (fun x0 ->
+ sk ((x0,s),true) fk))
(** val run :
'a1 t -> logicalEnvironment ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 20:22:14 +0000