63 open Hints_declaration
79 val ptr_type : Csyntax.type0 -> Nat.nat Types.option -> Csyntax.type0
81 type 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
85 | Add_case_ip of Nat.nat Types.option * AST.intsize * AST.signedness
87 | Add_default of Csyntax.type0 * Csyntax.type0
89 val 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
96 val 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
103 val 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
110 val 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
117 val 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
124 val 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
131 val 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 -> __ -> __ -> __
139 val 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 -> __ -> __ -> __
147 val 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 -> __ -> __ -> __
155 val 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 -> __ -> __ -> __
163 val 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 -> __ -> __ -> __
171 val classify_add_cases_discr :
172 Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> classify_add_cases
175 val classify_add_cases_jmdiscr :
176 Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> classify_add_cases
179 val classify_add : Csyntax.type0 -> Csyntax.type0 -> classify_add_cases
181 type 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
185 | Sub_case_pp of Nat.nat Types.option * Nat.nat Types.option * Csyntax.type0
187 | Sub_default of Csyntax.type0 * Csyntax.type0
189 val 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
196 val 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
203 val 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
210 val 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
217 val 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
224 val 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
231 val 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
239 val 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
247 val 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
255 val 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
263 val 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
271 val classify_sub_cases_discr :
272 Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> classify_sub_cases
275 val classify_sub_cases_jmdiscr :
276 Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> classify_sub_cases
279 val classify_sub : Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases
281 type classify_aop_cases =
282 | Aop_case_ii of AST.intsize * AST.signedness
283 | Aop_default of Csyntax.type0 * Csyntax.type0
285 val 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
289 val 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
293 val 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
297 val 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
301 val 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
305 val 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
309 val 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
314 val 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
319 val 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
324 val 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
329 val 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
334 val classify_aop_cases_discr :
335 Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> classify_aop_cases
338 val classify_aop_cases_jmdiscr :
339 Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> classify_aop_cases
342 val classify_aop : Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases
344 type 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
349 val 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
354 val 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
359 val 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
364 val 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
369 val 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
374 val 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
379 val 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
385 val 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
391 val 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
397 val 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
403 val 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
409 val classify_cmp_cases_discr :
410 Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> classify_cmp_cases
413 val classify_cmp_cases_jmdiscr :
414 Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> classify_cmp_cases
417 val classify_cmp : Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases
419 type classify_fun_cases =
420 | Fun_case_f of Csyntax.typelist * Csyntax.type0
423 val classify_fun_cases_rect_Type4 :
424 (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
427 val classify_fun_cases_rect_Type5 :
428 (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
431 val classify_fun_cases_rect_Type3 :
432 (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
435 val classify_fun_cases_rect_Type2 :
436 (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
439 val classify_fun_cases_rect_Type1 :
440 (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
443 val classify_fun_cases_rect_Type0 :
444 (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
447 val classify_fun_cases_inv_rect_Type4 :
448 classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
451 val classify_fun_cases_inv_rect_Type3 :
452 classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
455 val classify_fun_cases_inv_rect_Type2 :
456 classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
459 val classify_fun_cases_inv_rect_Type1 :
460 classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
463 val classify_fun_cases_inv_rect_Type0 :
464 classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
467 val classify_fun_cases_discr : classify_fun_cases -> classify_fun_cases -> __
469 val classify_fun_cases_jmdiscr :
470 classify_fun_cases -> classify_fun_cases -> __
472 val classify_fun : Csyntax.type0 -> classify_fun_cases