source: extracted/smallstep.ml @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 16.8 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open Extralib
12
13open Lists
14
15open Identifiers
16
17open Floats
18
19open Integers
20
21open AST
22
23open Division
24
25open Arithmetic
26
27open Extranat
28
29open Vector
30
31open FoldStuff
32
33open BitVector
34
35open Z
36
37open BitVectorZ
38
39open Pointers
40
41open Option
42
43open Setoids
44
45open Monad
46
47open Positive
48
49open Char
50
51open String
52
53open PreIdentifiers
54
55open Errors
56
57open Div_and_mod
58
59open Jmeq
60
61open Russell
62
63open Util
64
65open Bool
66
67open Relations
68
69open Nat
70
71open List
72
73open Hints_declaration
74
75open Core_notation
76
77open Pts
78
79open Logic
80
81open Types
82
83open Coqlib
84
85open Values
86
87open Events
88
89type transrel =
90| Mk_transrel
91
92(** val transrel_rect_Type4 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
93let rec transrel_rect_Type4 h_mk_transrel = function
94| Mk_transrel -> h_mk_transrel __ __ __
95
96(** val transrel_rect_Type5 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
97let rec transrel_rect_Type5 h_mk_transrel = function
98| Mk_transrel -> h_mk_transrel __ __ __
99
100(** val transrel_rect_Type3 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
101let rec transrel_rect_Type3 h_mk_transrel = function
102| Mk_transrel -> h_mk_transrel __ __ __
103
104(** val transrel_rect_Type2 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
105let rec transrel_rect_Type2 h_mk_transrel = function
106| Mk_transrel -> h_mk_transrel __ __ __
107
108(** val transrel_rect_Type1 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
109let rec transrel_rect_Type1 h_mk_transrel = function
110| Mk_transrel -> h_mk_transrel __ __ __
111
112(** val transrel_rect_Type0 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1 **)
113let rec transrel_rect_Type0 h_mk_transrel = function
114| Mk_transrel -> h_mk_transrel __ __ __
115
116type genv = __
117
118type state = __
119
120type step = __
121
122(** val transrel_inv_rect_Type4 :
123    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
124let transrel_inv_rect_Type4 hterm h1 =
125  let hcut = transrel_rect_Type4 h1 hterm in hcut __
126
127(** val transrel_inv_rect_Type3 :
128    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
129let transrel_inv_rect_Type3 hterm h1 =
130  let hcut = transrel_rect_Type3 h1 hterm in hcut __
131
132(** val transrel_inv_rect_Type2 :
133    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
134let transrel_inv_rect_Type2 hterm h1 =
135  let hcut = transrel_rect_Type2 h1 hterm in hcut __
136
137(** val transrel_inv_rect_Type1 :
138    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
139let transrel_inv_rect_Type1 hterm h1 =
140  let hcut = transrel_rect_Type1 h1 hterm in hcut __
141
142(** val transrel_inv_rect_Type0 :
143    transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
144let transrel_inv_rect_Type0 hterm h1 =
145  let hcut = transrel_rect_Type0 h1 hterm in hcut __
146
147(** val transrel_jmdiscr : transrel -> transrel -> __ **)
148let transrel_jmdiscr x y =
149  Logic.eq_rect_Type2 x
150    (let Mk_transrel = x in Obj.magic (fun _ dH -> dH __ __ __)) y
151
152type program_behavior =
153| Terminates of Events.trace * Integers.int
154| Diverges of Events.trace
155| Reacts of Events.traceinf
156| Goes_wrong of Events.trace
157
158(** val program_behavior_rect_Type4 :
159    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
160    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
161    'a1 **)
162let rec program_behavior_rect_Type4 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
163| Terminates (x_5847, x_5846) -> h_Terminates x_5847 x_5846
164| Diverges x_5848 -> h_Diverges x_5848
165| Reacts x_5849 -> h_Reacts x_5849
166| Goes_wrong x_5850 -> h_Goes_wrong x_5850
167
168(** val program_behavior_rect_Type5 :
169    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
170    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
171    'a1 **)
172let rec program_behavior_rect_Type5 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
173| Terminates (x_5857, x_5856) -> h_Terminates x_5857 x_5856
174| Diverges x_5858 -> h_Diverges x_5858
175| Reacts x_5859 -> h_Reacts x_5859
176| Goes_wrong x_5860 -> h_Goes_wrong x_5860
177
178(** val program_behavior_rect_Type3 :
179    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
180    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
181    'a1 **)
182let rec program_behavior_rect_Type3 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
183| Terminates (x_5867, x_5866) -> h_Terminates x_5867 x_5866
184| Diverges x_5868 -> h_Diverges x_5868
185| Reacts x_5869 -> h_Reacts x_5869
186| Goes_wrong x_5870 -> h_Goes_wrong x_5870
187
188(** val program_behavior_rect_Type2 :
189    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
190    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
191    'a1 **)
192let rec program_behavior_rect_Type2 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
193| Terminates (x_5877, x_5876) -> h_Terminates x_5877 x_5876
194| Diverges x_5878 -> h_Diverges x_5878
195| Reacts x_5879 -> h_Reacts x_5879
196| Goes_wrong x_5880 -> h_Goes_wrong x_5880
197
198(** val program_behavior_rect_Type1 :
199    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
200    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
201    'a1 **)
202let rec program_behavior_rect_Type1 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
203| Terminates (x_5887, x_5886) -> h_Terminates x_5887 x_5886
204| Diverges x_5888 -> h_Diverges x_5888
205| Reacts x_5889 -> h_Reacts x_5889
206| Goes_wrong x_5890 -> h_Goes_wrong x_5890
207
208(** val program_behavior_rect_Type0 :
209    (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
210    (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
211    'a1 **)
212let rec program_behavior_rect_Type0 h_Terminates h_Diverges h_Reacts h_Goes_wrong = function
213| Terminates (x_5897, x_5896) -> h_Terminates x_5897 x_5896
214| Diverges x_5898 -> h_Diverges x_5898
215| Reacts x_5899 -> h_Reacts x_5899
216| Goes_wrong x_5900 -> h_Goes_wrong x_5900
217
218(** val program_behavior_inv_rect_Type4 :
219    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
220    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
221    (Events.trace -> __ -> 'a1) -> 'a1 **)
222let program_behavior_inv_rect_Type4 hterm h1 h2 h3 h4 =
223  let hcut = program_behavior_rect_Type4 h1 h2 h3 h4 hterm in hcut __
224
225(** val program_behavior_inv_rect_Type3 :
226    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
227    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
228    (Events.trace -> __ -> 'a1) -> 'a1 **)
229let program_behavior_inv_rect_Type3 hterm h1 h2 h3 h4 =
230  let hcut = program_behavior_rect_Type3 h1 h2 h3 h4 hterm in hcut __
231
232(** val program_behavior_inv_rect_Type2 :
233    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
234    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
235    (Events.trace -> __ -> 'a1) -> 'a1 **)
236let program_behavior_inv_rect_Type2 hterm h1 h2 h3 h4 =
237  let hcut = program_behavior_rect_Type2 h1 h2 h3 h4 hterm in hcut __
238
239(** val program_behavior_inv_rect_Type1 :
240    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
241    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
242    (Events.trace -> __ -> 'a1) -> 'a1 **)
243let program_behavior_inv_rect_Type1 hterm h1 h2 h3 h4 =
244  let hcut = program_behavior_rect_Type1 h1 h2 h3 h4 hterm in hcut __
245
246(** val program_behavior_inv_rect_Type0 :
247    program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
248    (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
249    (Events.trace -> __ -> 'a1) -> 'a1 **)
250let program_behavior_inv_rect_Type0 hterm h1 h2 h3 h4 =
251  let hcut = program_behavior_rect_Type0 h1 h2 h3 h4 hterm in hcut __
252
253(** val program_behavior_discr :
254    program_behavior -> program_behavior -> __ **)
255let program_behavior_discr x y =
256  Logic.eq_rect_Type2 x
257    (match x with
258     | Terminates (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
259     | Diverges a0 -> Obj.magic (fun _ dH -> dH __)
260     | Reacts a0 -> Obj.magic (fun _ dH -> dH __)
261     | Goes_wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
262
263(** val program_behavior_jmdiscr :
264    program_behavior -> program_behavior -> __ **)
265let program_behavior_jmdiscr x y =
266  Logic.eq_rect_Type2 x
267    (match x with
268     | Terminates (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
269     | Diverges a0 -> Obj.magic (fun _ dH -> dH __)
270     | Reacts a0 -> Obj.magic (fun _ dH -> dH __)
271     | Goes_wrong a0 -> Obj.magic (fun _ dH -> dH __)) y
272
273type semantics = { trans : transrel; ge : __ }
274
275(** val semantics_rect_Type4 :
276    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
277let rec semantics_rect_Type4 h_mk_semantics x_6227 =
278  let { trans = trans0; ge = ge0 } = x_6227 in
279  h_mk_semantics trans0 __ __ ge0
280
281(** val semantics_rect_Type5 :
282    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
283let rec semantics_rect_Type5 h_mk_semantics x_6229 =
284  let { trans = trans0; ge = ge0 } = x_6229 in
285  h_mk_semantics trans0 __ __ ge0
286
287(** val semantics_rect_Type3 :
288    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
289let rec semantics_rect_Type3 h_mk_semantics x_6231 =
290  let { trans = trans0; ge = ge0 } = x_6231 in
291  h_mk_semantics trans0 __ __ ge0
292
293(** val semantics_rect_Type2 :
294    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
295let rec semantics_rect_Type2 h_mk_semantics x_6233 =
296  let { trans = trans0; ge = ge0 } = x_6233 in
297  h_mk_semantics trans0 __ __ ge0
298
299(** val semantics_rect_Type1 :
300    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
301let rec semantics_rect_Type1 h_mk_semantics x_6235 =
302  let { trans = trans0; ge = ge0 } = x_6235 in
303  h_mk_semantics trans0 __ __ ge0
304
305(** val semantics_rect_Type0 :
306    (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1 **)
307let rec semantics_rect_Type0 h_mk_semantics x_6237 =
308  let { trans = trans0; ge = ge0 } = x_6237 in
309  h_mk_semantics trans0 __ __ ge0
310
311(** val trans : semantics -> transrel **)
312let rec trans xxx =
313  xxx.trans
314
315type initial = __
316
317type final = __
318
319(** val ge : semantics -> __ **)
320let rec ge xxx =
321  xxx.ge
322
323(** val semantics_inv_rect_Type4 :
324    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
325let semantics_inv_rect_Type4 hterm h1 =
326  let hcut = semantics_rect_Type4 h1 hterm in hcut __
327
328(** val semantics_inv_rect_Type3 :
329    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
330let semantics_inv_rect_Type3 hterm h1 =
331  let hcut = semantics_rect_Type3 h1 hterm in hcut __
332
333(** val semantics_inv_rect_Type2 :
334    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
335let semantics_inv_rect_Type2 hterm h1 =
336  let hcut = semantics_rect_Type2 h1 hterm in hcut __
337
338(** val semantics_inv_rect_Type1 :
339    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
340let semantics_inv_rect_Type1 hterm h1 =
341  let hcut = semantics_rect_Type1 h1 hterm in hcut __
342
343(** val semantics_inv_rect_Type0 :
344    semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
345let semantics_inv_rect_Type0 hterm h1 =
346  let hcut = semantics_rect_Type0 h1 hterm in hcut __
347
348(** val semantics_jmdiscr : semantics -> semantics -> __ **)
349let semantics_jmdiscr x y =
350  Logic.eq_rect_Type2 x
351    (let { trans = a0; ge = a3 } = x in
352    Obj.magic (fun _ dH -> dH __ __ __ __)) y
353
354type related_semantics = { sem1 : semantics; sem2 : semantics }
355
356(** val related_semantics_rect_Type4 :
357    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
358    'a1 **)
359let rec related_semantics_rect_Type4 h_mk_related_semantics x_6256 =
360  let { sem1 = sem3; sem2 = sem4 } = x_6256 in
361  h_mk_related_semantics sem3 sem4 __ __ __
362
363(** val related_semantics_rect_Type5 :
364    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
365    'a1 **)
366let rec related_semantics_rect_Type5 h_mk_related_semantics x_6258 =
367  let { sem1 = sem3; sem2 = sem4 } = x_6258 in
368  h_mk_related_semantics sem3 sem4 __ __ __
369
370(** val related_semantics_rect_Type3 :
371    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
372    'a1 **)
373let rec related_semantics_rect_Type3 h_mk_related_semantics x_6260 =
374  let { sem1 = sem3; sem2 = sem4 } = x_6260 in
375  h_mk_related_semantics sem3 sem4 __ __ __
376
377(** val related_semantics_rect_Type2 :
378    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
379    'a1 **)
380let rec related_semantics_rect_Type2 h_mk_related_semantics x_6262 =
381  let { sem1 = sem3; sem2 = sem4 } = x_6262 in
382  h_mk_related_semantics sem3 sem4 __ __ __
383
384(** val related_semantics_rect_Type1 :
385    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
386    'a1 **)
387let rec related_semantics_rect_Type1 h_mk_related_semantics x_6264 =
388  let { sem1 = sem3; sem2 = sem4 } = x_6264 in
389  h_mk_related_semantics sem3 sem4 __ __ __
390
391(** val related_semantics_rect_Type0 :
392    (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
393    'a1 **)
394let rec related_semantics_rect_Type0 h_mk_related_semantics x_6266 =
395  let { sem1 = sem3; sem2 = sem4 } = x_6266 in
396  h_mk_related_semantics sem3 sem4 __ __ __
397
398(** val sem1 : related_semantics -> semantics **)
399let rec sem1 xxx =
400  xxx.sem1
401
402(** val sem2 : related_semantics -> semantics **)
403let rec sem2 xxx =
404  xxx.sem2
405
406type match_states = __
407
408(** val related_semantics_inv_rect_Type4 :
409    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
410    'a1) -> 'a1 **)
411let related_semantics_inv_rect_Type4 hterm h1 =
412  let hcut = related_semantics_rect_Type4 h1 hterm in hcut __
413
414(** val related_semantics_inv_rect_Type3 :
415    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
416    'a1) -> 'a1 **)
417let related_semantics_inv_rect_Type3 hterm h1 =
418  let hcut = related_semantics_rect_Type3 h1 hterm in hcut __
419
420(** val related_semantics_inv_rect_Type2 :
421    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
422    'a1) -> 'a1 **)
423let related_semantics_inv_rect_Type2 hterm h1 =
424  let hcut = related_semantics_rect_Type2 h1 hterm in hcut __
425
426(** val related_semantics_inv_rect_Type1 :
427    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
428    'a1) -> 'a1 **)
429let related_semantics_inv_rect_Type1 hterm h1 =
430  let hcut = related_semantics_rect_Type1 h1 hterm in hcut __
431
432(** val related_semantics_inv_rect_Type0 :
433    related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
434    'a1) -> 'a1 **)
435let related_semantics_inv_rect_Type0 hterm h1 =
436  let hcut = related_semantics_rect_Type0 h1 hterm in hcut __
437
438(** val related_semantics_jmdiscr :
439    related_semantics -> related_semantics -> __ **)
440let related_semantics_jmdiscr x y =
441  Logic.eq_rect_Type2 x
442    (let { sem1 = a0; sem2 = a1 } = x in
443    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
444
445type order_sim =
446  related_semantics
447  (* singleton inductive, whose constructor was mk_order_sim *)
448
449(** val order_sim_rect_Type4 :
450    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
451let rec order_sim_rect_Type4 h_mk_order_sim x_6287 =
452  let sem = x_6287 in h_mk_order_sim sem __ __
453
454(** val order_sim_rect_Type5 :
455    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
456let rec order_sim_rect_Type5 h_mk_order_sim x_6289 =
457  let sem = x_6289 in h_mk_order_sim sem __ __
458
459(** val order_sim_rect_Type3 :
460    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
461let rec order_sim_rect_Type3 h_mk_order_sim x_6291 =
462  let sem = x_6291 in h_mk_order_sim sem __ __
463
464(** val order_sim_rect_Type2 :
465    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
466let rec order_sim_rect_Type2 h_mk_order_sim x_6293 =
467  let sem = x_6293 in h_mk_order_sim sem __ __
468
469(** val order_sim_rect_Type1 :
470    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
471let rec order_sim_rect_Type1 h_mk_order_sim x_6295 =
472  let sem = x_6295 in h_mk_order_sim sem __ __
473
474(** val order_sim_rect_Type0 :
475    (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1 **)
476let rec order_sim_rect_Type0 h_mk_order_sim x_6297 =
477  let sem = x_6297 in h_mk_order_sim sem __ __
478
479(** val sem : order_sim -> related_semantics **)
480let rec sem xxx =
481  let yyy = xxx in yyy
482
483type order = __
484
485(** val order_sim_inv_rect_Type4 :
486    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
487let order_sim_inv_rect_Type4 hterm h1 =
488  let hcut = order_sim_rect_Type4 h1 hterm in hcut __
489
490(** val order_sim_inv_rect_Type3 :
491    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
492let order_sim_inv_rect_Type3 hterm h1 =
493  let hcut = order_sim_rect_Type3 h1 hterm in hcut __
494
495(** val order_sim_inv_rect_Type2 :
496    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
497let order_sim_inv_rect_Type2 hterm h1 =
498  let hcut = order_sim_rect_Type2 h1 hterm in hcut __
499
500(** val order_sim_inv_rect_Type1 :
501    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
502let order_sim_inv_rect_Type1 hterm h1 =
503  let hcut = order_sim_rect_Type1 h1 hterm in hcut __
504
505(** val order_sim_inv_rect_Type0 :
506    order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1 **)
507let order_sim_inv_rect_Type0 hterm h1 =
508  let hcut = order_sim_rect_Type0 h1 hterm in hcut __
509
510(** val order_sim_jmdiscr : order_sim -> order_sim -> __ **)
511let order_sim_jmdiscr x y =
512  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __)) y
513
Note: See TracBrowser for help on using the repository browser.