blob: 9692bc631bcc581b8ceca04c4152072d68a467e1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
module Int : sig type t = int val compare : int -> int -> int val equal : int -> int -> bool end
module ISet : sig
include Set.S with type elt = int
val pp : out_channel -> t -> unit
end
module IMap :
sig
include Map.S with type key = int
(** [from k m] returns the submap of [m] with keys greater or equal k *)
val from : key -> 'elt t -> 'elt t
end
val numerator : Num.num -> Big_int.big_int
val denominator : Num.num -> Big_int.big_int
module Cmp : sig
val compare_list : ('a -> 'b -> int) -> 'a list -> 'b list -> int
val compare_lexical : (unit -> int) list -> int
end
module Tag : sig
type t
val pp : out_channel -> t -> unit
val next : t -> t
val max : t -> t -> t
val from : int -> t
val to_int : t -> int
end
module TagSet : CSig.SetS with type elt = Tag.t
val pp_list : string -> (out_channel -> 'a -> unit) -> out_channel -> 'a list -> unit
module CamlToCoq : sig
val positive : int -> Micromega.positive
val bigint : Big_int.big_int -> Micromega.z
val n : int -> Micromega.n
val nat : int -> Micromega.nat
val q : Num.num -> Micromega.q
val index : int -> Micromega.positive
val z : int -> Micromega.z
val positive_big_int : Big_int.big_int -> Micromega.positive
end
module CoqToCaml : sig
val z_big_int : Micromega.z -> Big_int.big_int
val z : Micromega.z -> int
val q_to_num : Micromega.q -> Num.num
val positive : Micromega.positive -> int
val n : Micromega.n -> int
val nat : Micromega.nat -> int
val index : Micromega.positive -> int
end
module Hash : sig
val eq_op1 : Micromega.op1 -> Micromega.op1 -> bool
val eq_positive : Micromega.positive -> Micromega.positive -> bool
val eq_z : Micromega.z -> Micromega.z -> bool
val eq_q : Micromega.q -> Micromega.q -> bool
val eq_pol : ('a -> 'a -> bool) -> 'a Micromega.pol -> 'a Micromega.pol -> bool
val eq_pair : ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> 'a * 'b -> 'a * 'b -> bool
val hash_op1 : int -> Micromega.op1 -> int
val hash_pol : (int -> 'a -> int) -> int -> 'a Micromega.pol -> int
val hash_pair : (int -> 'a -> int) -> (int -> 'b -> int) -> int -> 'a * 'b -> int
val hash_z : int -> Micromega.z -> int
val hash_q : int -> Micromega.q -> int
val hash_string : int -> string -> int
val hash_elt : ('a -> int) -> int -> 'a -> int
end
val ppcm : Big_int.big_int -> Big_int.big_int -> Big_int.big_int
val all_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list
val try_any : (('a -> 'b option) * 'c) list -> 'a -> 'b option
val is_sublist : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val extract : ('a -> 'b option) -> 'a list -> ('b * 'a) option * 'a list
val extract_all : ('a -> 'b option) -> 'a list -> ('b * 'a) list * 'a list
val extract_best : ('a -> 'b option) -> ('b -> 'b -> bool) -> 'a list -> ('b *'a) option * 'a list
val find_some : ('a -> 'b option) -> 'a list -> 'b option
val iterate_until_stable : ('a -> 'a option) -> 'a -> 'a
val simplify : ('a -> 'a option) -> 'a list -> 'a list option
val saturate : ('a -> 'b option) -> ('b * 'a -> 'a -> 'a option) -> 'a list -> 'a list
val generate : ('a -> 'b option) -> 'a list -> 'b list
val app_funs : ('a -> 'b option) list -> 'a -> 'b option
val command : string -> string array -> 'a -> 'b
|
