Changeset 2743 for extracted/bindLists.ml

Timestamp:

Feb 27, 2013, 9:27:58 PM (8 years ago)

Author:

sacerdot

Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:

• extracted/bindLists.ml (modified) (1 diff)

extracted/bindLists.ml

@@ -33 +33 @@
 type ('b, 'e) bind_list = ('b, 'e List.list) Bind_new.bind_new
 
+(** val dpi1__o__blist_from_list__o__inject :
+    ('a2 List.list, 'a3) Types.dPair -> ('a1, 'a2 List.list)
+    Bind_new.bind_new Types.sig0 **)
+let dpi1__o__blist_from_list__o__inject x4 =
+  Bind_new.Bret x4.Types.dpi1
+
+(** val eject__o__blist_from_list__o__inject :
+    'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new
+    Types.sig0 **)
+let eject__o__blist_from_list__o__inject x4 =
+  Bind_new.Bret (Types.pi1 x4)
+
+(** val blist_from_list__o__inject :
+    'a2 List.list -> ('a1, 'a2 List.list) Bind_new.bind_new Types.sig0 **)
+let blist_from_list__o__inject x3 =
+  Bind_new.Bret x3
+
+(** val dpi1__o__blist_from_list :
+    ('a2 List.list, 'a3) Types.dPair -> ('a1, 'a2 List.list)
+    Bind_new.bind_new **)
+let dpi1__o__blist_from_list x3 =
+  let l = x3.Types.dpi1 in Bind_new.Bret l
+
+(** val eject__o__blist_from_list :
+    'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new **)
+let eject__o__blist_from_list x3 =
+  let l = Types.pi1 x3 in Bind_new.Bret l
+
 (** val bappend :
     ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list **)