source: driver/extracted/classifyOp.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 18.0 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
27open Exp
28
29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Setoids
48
49open Monad
50
51open Option
52
53open Extranat
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Integers
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open AST
74
75open Csyntax
76
77open TypeComparison
78
79val ptr_type : Csyntax.type0 -> Nat.nat Types.option -> Csyntax.type0
80
81type classify_add_cases =
82| Add_case_ii of AST.intsize * AST.signedness
83| Add_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
84   * AST.signedness
85| Add_case_ip of Nat.nat Types.option * AST.intsize * AST.signedness
86   * Csyntax.type0
87| Add_default of Csyntax.type0 * Csyntax.type0
88
89val classify_add_cases_rect_Type4 :
90  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
91  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
92  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
93  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
94  -> classify_add_cases -> 'a1
95
96val classify_add_cases_rect_Type5 :
97  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
98  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
99  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
100  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
101  -> classify_add_cases -> 'a1
102
103val classify_add_cases_rect_Type3 :
104  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
105  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
106  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
107  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
108  -> classify_add_cases -> 'a1
109
110val classify_add_cases_rect_Type2 :
111  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
112  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
113  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
114  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
115  -> classify_add_cases -> 'a1
116
117val classify_add_cases_rect_Type1 :
118  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
119  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
120  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
121  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
122  -> classify_add_cases -> 'a1
123
124val classify_add_cases_rect_Type0 :
125  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
126  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
127  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
128  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
129  -> classify_add_cases -> 'a1
130
131val classify_add_cases_inv_rect_Type4 :
132  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
133  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
134  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
135  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
136  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
137  -> 'a1) -> 'a1
138
139val classify_add_cases_inv_rect_Type3 :
140  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
141  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
142  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
143  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
144  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
145  -> 'a1) -> 'a1
146
147val classify_add_cases_inv_rect_Type2 :
148  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
149  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
150  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
151  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
152  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
153  -> 'a1) -> 'a1
154
155val classify_add_cases_inv_rect_Type1 :
156  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
157  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
158  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
159  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
160  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
161  -> 'a1) -> 'a1
162
163val classify_add_cases_inv_rect_Type0 :
164  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
165  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
166  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
167  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
168  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
169  -> 'a1) -> 'a1
170
171val classify_add_cases_discr :
172  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> classify_add_cases
173  -> __
174
175val classify_add_cases_jmdiscr :
176  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> classify_add_cases
177  -> __
178
179val classify_add : Csyntax.type0 -> Csyntax.type0 -> classify_add_cases
180
181type classify_sub_cases =
182| Sub_case_ii of AST.intsize * AST.signedness
183| Sub_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
184   * AST.signedness
185| Sub_case_pp of Nat.nat Types.option * Nat.nat Types.option * Csyntax.type0
186   * Csyntax.type0
187| Sub_default of Csyntax.type0 * Csyntax.type0
188
189val classify_sub_cases_rect_Type4 :
190  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
191  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
192  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
193  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
194  Csyntax.type0 -> classify_sub_cases -> 'a1
195
196val classify_sub_cases_rect_Type5 :
197  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
198  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
199  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
200  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
201  Csyntax.type0 -> classify_sub_cases -> 'a1
202
203val classify_sub_cases_rect_Type3 :
204  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
205  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
206  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
207  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
208  Csyntax.type0 -> classify_sub_cases -> 'a1
209
210val classify_sub_cases_rect_Type2 :
211  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
212  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
213  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
214  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
215  Csyntax.type0 -> classify_sub_cases -> 'a1
216
217val classify_sub_cases_rect_Type1 :
218  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
219  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
220  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
221  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
222  Csyntax.type0 -> classify_sub_cases -> 'a1
223
224val classify_sub_cases_rect_Type0 :
225  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
226  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
227  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
228  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
229  Csyntax.type0 -> classify_sub_cases -> 'a1
230
231val classify_sub_cases_inv_rect_Type4 :
232  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
233  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
234  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
235  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
236  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
237  -> __ -> __ -> __ -> 'a1) -> 'a1
238
239val classify_sub_cases_inv_rect_Type3 :
240  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
241  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
242  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
243  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
244  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
245  -> __ -> __ -> __ -> 'a1) -> 'a1
246
247val classify_sub_cases_inv_rect_Type2 :
248  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
249  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
250  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
251  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
252  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
253  -> __ -> __ -> __ -> 'a1) -> 'a1
254
255val classify_sub_cases_inv_rect_Type1 :
256  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
257  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
258  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
259  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
260  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
261  -> __ -> __ -> __ -> 'a1) -> 'a1
262
263val classify_sub_cases_inv_rect_Type0 :
264  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
265  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
266  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
267  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
268  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
269  -> __ -> __ -> __ -> 'a1) -> 'a1
270
271val classify_sub_cases_discr :
272  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> classify_sub_cases
273  -> __
274
275val classify_sub_cases_jmdiscr :
276  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> classify_sub_cases
277  -> __
278
279val classify_sub : Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases
280
281type classify_aop_cases =
282| Aop_case_ii of AST.intsize * AST.signedness
283| Aop_default of Csyntax.type0 * Csyntax.type0
284
285val classify_aop_cases_rect_Type4 :
286  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
287  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
288
289val classify_aop_cases_rect_Type5 :
290  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
291  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
292
293val classify_aop_cases_rect_Type3 :
294  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
295  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
296
297val classify_aop_cases_rect_Type2 :
298  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
299  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
300
301val classify_aop_cases_rect_Type1 :
302  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
303  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
304
305val classify_aop_cases_rect_Type0 :
306  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
307  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
308
309val classify_aop_cases_inv_rect_Type4 :
310  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
311  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
312  -> __ -> __ -> __ -> 'a1) -> 'a1
313
314val classify_aop_cases_inv_rect_Type3 :
315  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
316  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
317  -> __ -> __ -> __ -> 'a1) -> 'a1
318
319val classify_aop_cases_inv_rect_Type2 :
320  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
321  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
322  -> __ -> __ -> __ -> 'a1) -> 'a1
323
324val classify_aop_cases_inv_rect_Type1 :
325  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
326  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
327  -> __ -> __ -> __ -> 'a1) -> 'a1
328
329val classify_aop_cases_inv_rect_Type0 :
330  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
331  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
332  -> __ -> __ -> __ -> 'a1) -> 'a1
333
334val classify_aop_cases_discr :
335  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> classify_aop_cases
336  -> __
337
338val classify_aop_cases_jmdiscr :
339  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> classify_aop_cases
340  -> __
341
342val classify_aop : Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases
343
344type classify_cmp_cases =
345| Cmp_case_ii of AST.intsize * AST.signedness
346| Cmp_case_pp of Nat.nat Types.option * Csyntax.type0
347| Cmp_default of Csyntax.type0 * Csyntax.type0
348
349val classify_cmp_cases_rect_Type4 :
350  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
351  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
352  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
353
354val classify_cmp_cases_rect_Type5 :
355  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
356  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
357  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
358
359val classify_cmp_cases_rect_Type3 :
360  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
361  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
362  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
363
364val classify_cmp_cases_rect_Type2 :
365  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
366  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
367  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
368
369val classify_cmp_cases_rect_Type1 :
370  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
371  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
372  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
373
374val classify_cmp_cases_rect_Type0 :
375  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
376  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
377  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
378
379val classify_cmp_cases_inv_rect_Type4 :
380  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
381  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
382  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
383  -> __ -> __ -> __ -> 'a1) -> 'a1
384
385val classify_cmp_cases_inv_rect_Type3 :
386  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
387  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
388  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
389  -> __ -> __ -> __ -> 'a1) -> 'a1
390
391val classify_cmp_cases_inv_rect_Type2 :
392  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
393  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
394  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
395  -> __ -> __ -> __ -> 'a1) -> 'a1
396
397val classify_cmp_cases_inv_rect_Type1 :
398  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
399  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
400  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
401  -> __ -> __ -> __ -> 'a1) -> 'a1
402
403val classify_cmp_cases_inv_rect_Type0 :
404  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
405  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
406  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
407  -> __ -> __ -> __ -> 'a1) -> 'a1
408
409val classify_cmp_cases_discr :
410  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> classify_cmp_cases
411  -> __
412
413val classify_cmp_cases_jmdiscr :
414  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> classify_cmp_cases
415  -> __
416
417val classify_cmp : Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases
418
419type classify_fun_cases =
420| Fun_case_f of Csyntax.typelist * Csyntax.type0
421| Fun_default
422
423val classify_fun_cases_rect_Type4 :
424  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
425  'a1
426
427val classify_fun_cases_rect_Type5 :
428  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
429  'a1
430
431val classify_fun_cases_rect_Type3 :
432  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
433  'a1
434
435val classify_fun_cases_rect_Type2 :
436  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
437  'a1
438
439val classify_fun_cases_rect_Type1 :
440  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
441  'a1
442
443val classify_fun_cases_rect_Type0 :
444  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
445  'a1
446
447val classify_fun_cases_inv_rect_Type4 :
448  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
449  (__ -> 'a1) -> 'a1
450
451val classify_fun_cases_inv_rect_Type3 :
452  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
453  (__ -> 'a1) -> 'a1
454
455val classify_fun_cases_inv_rect_Type2 :
456  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
457  (__ -> 'a1) -> 'a1
458
459val classify_fun_cases_inv_rect_Type1 :
460  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
461  (__ -> 'a1) -> 'a1
462
463val classify_fun_cases_inv_rect_Type0 :
464  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
465  (__ -> 'a1) -> 'a1
466
467val classify_fun_cases_discr : classify_fun_cases -> classify_fun_cases -> __
468
469val classify_fun_cases_jmdiscr :
470  classify_fun_cases -> classify_fun_cases -> __
471
472val classify_fun : Csyntax.type0 -> classify_fun_cases
473
Note: See TracBrowser for help on using the repository browser.