Many bug fixed and improvements in minidom.

diff --git a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/.cvsignore b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/.cvsignore
new file mode 100644 (file)
index 0000000..84bdd8e
--- /dev/null
+++ b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/.cvsignore
@@ -0,0 +1 @@
+*.cmi *.cmo *.cmx test test.opt

diff --git a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/.cvsignore b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/.cvsignore
new file mode 100644 (file)
index 0000000..84bdd8e
--- /dev/null
+++ b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/.cvsignore
@@ -0,0 +1 @@
+*.cmi *.cmo *.cmx test test.opt

diff --git a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/minidom.mli b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/minidom.mli
index d37f62bd94537cb17120c10b7f9af39ad70839f4..0b655955b3f0f8d76d312c2962d1c4c982821225 100644 (file)
--- a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/minidom.mli
+++ b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/minidom.mli
@@ -15,9 +15,9 @@ external doc_unload : mDOMDoc -> unit = "ml_doc_unload"
 external doc_new : mDOMString -> mDOMDoc = "ml_doc_new"
 external doc_get_root_node : mDOMDoc -> mDOMNode = "ml_doc_get_root_node"
 
-external doc_add_entity : mDOMDoc -> mDOMString -> mDOMString -> mDOMEntity = "ml_doc_add_entity"
-external doc_get_entity : mDOMDoc -> mDOMString -> mDOMEntity option = "ml_doc_get_entity"
-external doc_get_predefined_entity : mDOMDoc -> mDOMString -> mDOMEntity option = "ml_doc_get_predefined_entity"
+external doc_add_entity : doc:mDOMDoc -> name:mDOMString -> content:mDOMString -> mDOMEntity = "ml_doc_add_entity"
+external doc_get_entity : doc:mDOMDoc -> name:mDOMString -> mDOMEntity option = "ml_doc_get_entity"
+external doc_get_predefined_entity : doc:mDOMDoc -> name:mDOMString -> mDOMEntity option = "ml_doc_get_predefined_entity"
 external entity_get_content : mDOMEntity -> mDOMString = "ml_entity_get_content"
 
 external node_is_text  : mDOMNode -> bool = "ml_node_is_text"
@@ -27,8 +27,8 @@ external node_is_entity_ref : mDOMNode -> bool = "ml_node_is_entity_ref"
 external node_get_type : mDOMNode -> int = "ml_node_get_type"
 external node_get_name : mDOMNode -> mDOMString option = "ml_node_get_name"
 external node_get_ns_uri : mDOMNode -> mDOMString option = "ml_node_get_ns_uri"
-external node_get_attribute : mDOMNode -> mDOMString -> mDOMString option = "ml_node_get_attribute"
-external node_get_attribute_ns : mDOMNode -> mDOMString -> mDOMString -> mDOMString option = "ml_node_get_attribute_ns"
+external node_get_attribute : node:mDOMNode -> name:mDOMString -> mDOMString option = "ml_node_get_attribute"
+external node_get_attribute_ns : node:mDOMNode -> name:mDOMString -> ns_uri:mDOMString -> mDOMString option = "ml_node_get_attribute_ns"
 external node_get_content : mDOMNode -> mDOMString option = "ml_node_get_content"
 external node_get_parent : mDOMNode -> mDOMNode option = "ml_node_get_parent"
 external node_get_prev_sibling : mDOMNode -> mDOMNode option = "ml_node_get_prev_sibling"

diff --git a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/ml_minidom.c b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/ml_minidom.c
index 2eb389fc1650d87d76bc200be648c89510e11480..10626143c01f1eaedb87476a8e324185b86f33c1 100644 (file)
--- a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/ml_minidom.c
+++ b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/ml_minidom.c
@@ -4,7 +4,11 @@
 #include <memory.h>
 
 #include "minidom.h"
-#include "ml_minidom.h"
+
+#define Val_ptr(p)        ((value) (p))
+#define Val_option(p,f)   ((p != NULL) ? ml_some(f(p)) : Val_unit)
+#define Val_mDOMString(s) (copy_string((char*) (s)))
+#define mDOMString_val(v) ((mDOMStringRef) String_val(v))
 
 static value
 ml_some(value v)
@@ -161,6 +165,13 @@ ml_node_get_name(value node)
   CAMLreturn(Val_option(mdom_node_get_name((mDOMNodeRef) node), Val_mDOMString));
 }
 
+value
+ml_node_get_content(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_option(mdom_node_get_content((mDOMNodeRef) node), Val_mDOMString));
+}
+
 value
 ml_node_get_ns_uri(value node)
 {

diff --git a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.ml b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.ml
index a1567864c7ae92054a083d9b42ce5eb06b62ad5e..3c7a092e9bfd7807441311ed44180ddeb386bf19 100644 (file)
--- a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.ml
+++ b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.ml
@@ -3,7 +3,82 @@ let doc = Minidom.doc_load "test.xml"
 
 let root = Minidom.doc_get_root_node doc
 
-let Some root_name = Minidom.node_get_name root
+let check_attribute_ns attr =
+  Printf.printf "\n\n";
+  let ns_uri = Minidom.attr_get_ns_uri attr
+  and attr_name = Minidom.attr_get_name attr
+  and attr_value = Minidom.attr_get_value attr
+  and parent = Minidom.attr_get_parent attr
+  in
+  match parent,ns_uri,attr_name,attr_value with
+    Some parent_node,Some uri,Some attribute_name,Some attribute_value ->
+      let attr_value = Minidom.node_get_attribute_ns parent_node attribute_name uri
+      in begin
+        match attr_value with
+          Some attr1 ->
+           Printf.printf "found the attribute with ns %s (was %s)\n"
+              (Minidom.string_of_mDOMString attr1) (Minidom.string_of_mDOMString attribute_value)
+        | None ->
+           Printf.printf "attribute not found (uri was %s)!!!!\n" (Minidom.string_of_mDOMString uri)
+      end
+  | _ ->
+      Printf.printf "parent_node == NULL || uri == NULL || attribute_name == NULL || attribute_value == NULL\n"
 ;;
+    
+let print_attribute attr =
+  check_attribute_ns attr;
+  let ns_uri = Minidom.attr_get_ns_uri attr
+  in
+  begin
+    match ns_uri with
+      Some uri -> Printf.printf " %s:" (Minidom.string_of_mDOMString uri);
+    | None -> ()
+  end;
+  match ((Minidom.attr_get_name attr), (Minidom.attr_get_value attr)) with
+    (Some attr_name, Some attr_value) ->
+      Printf.printf " %s=\"%s\"" (Minidom.string_of_mDOMString attr_name) (Minidom.string_of_mDOMString attr_value) 
+  | (Some attr_name, _) ->
+      Printf.printf " ??? attribute %s has no value !!!" (Minidom.string_of_mDOMString attr_name)
+  | (_,_) ->
+      Printf.printf " ??? very strange attribute !!!"
+;;
+
+let rec print_node n node =
+  if Minidom.node_is_blank node then ()
+  else if Minidom.node_is_element node then begin
+    match Minidom.node_get_name node with
+      Some node_name -> 
+        begin
+          let children = Minidom.node_get_children node
+          and attributes = Minidom.node_get_attributes node
+          and ns_uri = Minidom.node_get_ns_uri node
+          and is_first,is_last = (Minidom.node_is_first node), (Minidom.node_is_last node)
+          in
+          for i = 1 to n do print_char ' ' done;
+          Printf.printf "<";
+          begin
+            match ns_uri with
+              Some uri -> Printf.printf "%s:" (Minidom.string_of_mDOMString uri)
+            | None     -> ()
+          end;
+          Printf.printf "%s" (Minidom.string_of_mDOMString node_name);
+          List.iter print_attribute attributes;
+          Printf.printf ">\n";
+          List.iter (print_node (n + 2)) children;
+          for i = 1 to n do print_char ' ' done;
+          Printf.printf "</%s>\n" (Minidom.string_of_mDOMString node_name)
+        end
+    | None -> Printf.printf "??? this node has no name !!!\n"
+  end else if Minidom.node_is_text node then begin
+    match Minidom.node_get_content node with
+      Some node_content ->
+        for i = 1 to n do print_char ' ' done;
+        Printf.printf "%s\n" (Minidom.string_of_mDOMString node_content)
+    | None -> Printf.printf "??? this node has no content !!!\n"
+  end else begin
+    Printf.printf "don't know how to manage a node with type %d\n" (Minidom.node_get_type node)
+  end
+;;
+  
+print_node 0 root;;
 
-print_string (Minidom.string_of_mDOMString root_name)
\ No newline at end of file

diff --git a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.opt b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.opt
index f2dc0ec1e8834d9e548173d88dcc1da654f8b06d..20307125b44342b711b9933fe338588d085697d2 100755 (executable)
Binary files a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.opt and b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.opt differ

diff --git a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.xml b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.xml
index bdac517a30368dd310f899bd08f2293384685e32..83d2eef68bbdf76d2246b7993d56678810452f8d 100644 (file)
--- a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.xml
+++ b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.0/minidom/test.xml
@@ -1,3 +1,505 @@
-<prova>
-  <ciao/>
-</prova>
+<?xml version="1.0" encoding="iso-8859-1"?>
+<?cocoon-format type="text/xhtml"?>
+<m:math xmlns:helm="http://www.cs.unibo.it/helm" xmlns:m="http://www.w3.org/1998/Math/MathML">
+    <m:mtable helm:xref="i0" columnalign="left" equalrows="false" align="baseline 1">
+        <m:mtr>
+            <m:mtd>
+                <m:mrow>
+                    <m:mtext>DEFINITION and_ind() OF TYPE</m:mtext>
+                </m:mrow>
+            </m:mtd>
+        </m:mtr>
+        <m:mtr>
+            <m:mtd>
+                <m:mrow>
+                    <m:mphantom>
+                        <m:mtext>__</m:mtext>
+                    </m:mphantom>
+                    <m:semantics xmlns:xlink="http://www.w3.org/1999/xlink">
+                        <m:mrow helm:xref="i22">
+                            <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                <m:mtr>
+                                    <m:mtd>
+                                        <m:mrow>
+                                            <m:mo stretchy="false">(</m:mo>
+                                            <m:mrow helm:xref="i23">
+                                                <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                    <m:mtr>
+                                                        <m:mtd>
+                                                            <m:mo color="Blue">&#928;</m:mo>
+                                                            <m:mi>A</m:mi>
+                                                            <m:mo>:</m:mo>
+                                                            <m:mrow helm:xref="i24">
+                                                                <m:mo>Prop</m:mo>
+                                                            </m:mrow>
+                                                        </m:mtd>
+                                                    </m:mtr>
+                                                    <m:mtr>
+                                                        <m:mtd>
+                                                            <m:mrow>
+                                                                <m:mo>.</m:mo>
+                                                                <m:mrow helm:xref="i25">
+                                                                    <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                                        <m:mtr>
+                                                                            <m:mtd>
+                                                                                <m:mo color="Blue">&#928;</m:mo>
+                                                                                <m:mi>B</m:mi>
+                                                                                <m:mo>:</m:mo>
+                                                                                <m:mrow helm:xref="i26">
+                                                                                    <m:mo>Prop</m:mo>
+                                                                                </m:mrow>
+                                                                            </m:mtd>
+                                                                        </m:mtr>
+                                                                        <m:mtr>
+                                                                            <m:mtd>
+                                                                                <m:mrow>
+                                                                                    <m:mo>.</m:mo>
+                                                                                    <m:mrow helm:xref="i27">
+                                                                                        <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                                                            <m:mtr>
+                                                                                                <m:mtd>
+                                                                                                    <m:mo color="Blue">&#928;</m:mo>
+                                                                                                    <m:mi>P</m:mi>
+                                                                                                    <m:mo>:</m:mo>
+                                                                                                    <m:mrow helm:xref="i28">
+                                                                                                        <m:mo>Prop</m:mo>
+                                                                                                    </m:mrow>
+                                                                                                </m:mtd>
+                                                                                            </m:mtr>
+                                                                                            <m:mtr>
+                                                                                                <m:mtd>
+                                                                                                    <m:mrow>
+                                                                                                        <m:mo>.</m:mo>
+                                                                                                        <m:mrow helm:xref="i29">
+                                                                                                            <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                                                                                <m:mtr>
+                                                                                                                    <m:mtd>
+                                                                                                                        <m:mo color="Blue">&#928;</m:mo>
+                                                                                                                        <m:mi>f</m:mi>
+                                                                                                                        <m:mo>:</m:mo>
+                                                                                                                        <m:mrow helm:xref="i30">
+                                                                                                                            <m:mo stretchy="false">(</m:mo>
+                                                                                                                            <m:mi helm:xref="i31">A</m:mi>
+                                                                                                                            <m:mo color="Blue">&#8594;</m:mo>
+                                                                                                                            <m:mrow helm:xref="i32">
+                                                                                                                                <m:mo stretchy="false">(</m:mo>
+                                                                                                                                <m:mi helm:xref="i33">B</m:mi>
+                                                                                                                                <m:mo color="Blue">&#8594;</m:mo>
+                                                                                                                                <m:mi helm:xref="i34">P</m:mi>
+                                                                                                                                <m:mo stretchy="false">)</m:mo>
+                                                                                                                            </m:mrow>
+                                                                                                                            <m:mo stretchy="false">)</m:mo>
+                                                                                                                        </m:mrow>
+                                                                                                                    </m:mtd>
+                                                                                                                </m:mtr>
+                                                                                                                <m:mtr>
+                                                                                                                    <m:mtd>
+                                                                                                                        <m:mrow>
+                                                                                                                            <m:mo>.</m:mo>
+                                                                                                                            <m:mrow helm:xref="i35">
+                                                                                                                                <m:mo color="Blue">&#928;</m:mo>
+                                                                                                                                <m:mi>a</m:mi>
+                                                                                                                                <m:mo>:</m:mo>
+                                                                                                                                <m:mrow helm:xref="i36">
+                                                                                                                                    <m:mo stretchy="false">(</m:mo>
+                                                                                                                                    <m:mi xlink:href="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i37">and</m:mi>
+                                                                                                                                    <m:mphantom>
+                                                                                                                                        <m:mtext>_</m:mtext>
+                                                                                                                                    </m:mphantom>
+                                                                                                                                    <m:mi helm:xref="i38">A</m:mi>
+                                                                                                                                    <m:mphantom>
+                                                                                                                                        <m:mtext>_</m:mtext>
+                                                                                                                                    </m:mphantom>
+                                                                                                                                    <m:mi helm:xref="i39">B</m:mi>
+                                                                                                                                    <m:mo stretchy="false">)</m:mo>
+                                                                                                                                </m:mrow>
+                                                                                                                                <m:mo>.</m:mo>
+                                                                                                                                <m:mi helm:xref="i40">P</m:mi>
+                                                                                                                            </m:mrow>
+                                                                                                                        </m:mrow>
+                                                                                                                    </m:mtd>
+                                                                                                                </m:mtr>
+                                                                                                            </m:mtable>
+                                                                                                        </m:mrow>
+                                                                                                    </m:mrow>
+                                                                                                </m:mtd>
+                                                                                            </m:mtr>
+                                                                                        </m:mtable>
+                                                                                    </m:mrow>
+                                                                                </m:mrow>
+                                                                            </m:mtd>
+                                                                        </m:mtr>
+                                                                    </m:mtable>
+                                                                </m:mrow>
+                                                            </m:mrow>
+                                                        </m:mtd>
+                                                    </m:mtr>
+                                                </m:mtable>
+                                            </m:mrow>
+                                        </m:mrow>
+                                    </m:mtd>
+                                </m:mtr>
+                                <m:mtr>
+                                    <m:mtd>
+                                        <m:mrow>
+                                            <m:mo color="#b03060">:&gt;</m:mo>
+                                            <m:mrow helm:xref="i41">
+                                                <m:mo>Prop</m:mo>
+                                            </m:mrow>
+                                        </m:mrow>
+                                    </m:mtd>
+                                </m:mtr>
+                                <m:mtr>
+                                    <m:mtd>
+                                        <m:mrow>
+                                            <m:mo stretchy="false">)</m:mo>
+                                        </m:mrow>
+                                    </m:mtd>
+                                </m:mtr>
+                            </m:mtable>
+                        </m:mrow>
+                        <m:annotation-xml encoding="MathML">
+                            <m:apply helm:xref="i22">
+                                <m:csymbol>cast</m:csymbol>
+                                <m:apply helm:xref="i23">
+                                    <m:csymbol>prod</m:csymbol>
+                                    <m:bvar>
+                                        <m:ci>A</m:ci>
+                                        <m:type>
+                                            <m:apply helm:xref="i24">
+                                                <m:csymbol>Prop</m:csymbol>
+                                            </m:apply>
+                                        </m:type>
+                                    </m:bvar>
+                                    <m:apply helm:xref="i25">
+                                        <m:csymbol>prod</m:csymbol>
+                                        <m:bvar>
+                                            <m:ci>B</m:ci>
+                                            <m:type>
+                                                <m:apply helm:xref="i26">
+                                                    <m:csymbol>Prop</m:csymbol>
+                                                </m:apply>
+                                            </m:type>
+                                        </m:bvar>
+                                        <m:apply helm:xref="i27">
+                                            <m:csymbol>prod</m:csymbol>
+                                            <m:bvar>
+                                                <m:ci>P</m:ci>
+                                                <m:type>
+                                                    <m:apply helm:xref="i28">
+                                                        <m:csymbol>Prop</m:csymbol>
+                                                    </m:apply>
+                                                </m:type>
+                                            </m:bvar>
+                                            <m:apply helm:xref="i29">
+                                                <m:csymbol>prod</m:csymbol>
+                                                <m:bvar>
+                                                    <m:ci>f</m:ci>
+                                                    <m:type>
+                                                        <m:apply helm:xref="i30">
+                                                            <m:csymbol>arrow</m:csymbol>
+                                                            <m:ci helm:xref="i31">A</m:ci>
+                                                            <m:apply helm:xref="i32">
+                                                                <m:csymbol>arrow</m:csymbol>
+                                                                <m:ci helm:xref="i33">B</m:ci>
+                                                                <m:ci helm:xref="i34">P</m:ci>
+                                                            </m:apply>
+                                                        </m:apply>
+                                                    </m:type>
+                                                </m:bvar>
+                                                <m:apply helm:xref="i35">
+                                                    <m:csymbol>prod</m:csymbol>
+                                                    <m:bvar>
+                                                        <m:ci>a</m:ci>
+                                                        <m:type>
+                                                            <m:apply helm:xref="i36">
+                                                                <m:csymbol>app</m:csymbol>
+                                                                <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i37">and</m:ci>
+                                                                <m:ci helm:xref="i38">A</m:ci>
+                                                                <m:ci helm:xref="i39">B</m:ci>
+                                                            </m:apply>
+                                                        </m:type>
+                                                    </m:bvar>
+                                                    <m:ci helm:xref="i40">P</m:ci>
+                                                </m:apply>
+                                            </m:apply>
+                                        </m:apply>
+                                    </m:apply>
+                                </m:apply>
+                                <m:apply helm:xref="i41">
+                                    <m:csymbol>Prop</m:csymbol>
+                                </m:apply>
+                            </m:apply>
+                        </m:annotation-xml>
+                    </m:semantics>
+                </m:mrow>
+            </m:mtd>
+        </m:mtr>
+        <m:mtr>
+            <m:mtd>
+                <m:mrow>
+                    <m:mtext>AS</m:mtext>
+                </m:mrow>
+            </m:mtd>
+        </m:mtr>
+        <m:mtr>
+            <m:mtd>
+                <m:mrow>
+                    <m:mphantom>
+                        <m:mtext>__</m:mtext>
+                    </m:mphantom>
+                    <m:semantics xmlns:xlink="http://www.w3.org/1999/xlink">
+                        <m:mrow helm:xref="i1">
+                            <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                <m:mtr>
+                                    <m:mtd>
+                                        <m:mo color="Red">&#955;</m:mo>
+                                        <m:mi>A</m:mi>
+                                        <m:mo>:</m:mo>
+                                        <m:mrow helm:xref="i2">
+                                            <m:mo>Prop</m:mo>
+                                        </m:mrow>
+                                    </m:mtd>
+                                </m:mtr>
+                                <m:mtr>
+                                    <m:mtd>
+                                        <m:mrow>
+                                            <m:mo>.</m:mo>
+                                            <m:mrow helm:xref="i3">
+                                                <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                    <m:mtr>
+                                                        <m:mtd>
+                                                            <m:mo color="Red">&#955;</m:mo>
+                                                            <m:mi>B</m:mi>
+                                                            <m:mo>:</m:mo>
+                                                            <m:mrow helm:xref="i4">
+                                                                <m:mo>Prop</m:mo>
+                                                            </m:mrow>
+                                                        </m:mtd>
+                                                    </m:mtr>
+                                                    <m:mtr>
+                                                        <m:mtd>
+                                                            <m:mrow>
+                                                                <m:mo>.</m:mo>
+                                                                <m:mrow helm:xref="i5">
+                                                                    <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                                        <m:mtr>
+                                                                            <m:mtd>
+                                                                                <m:mo color="Red">&#955;</m:mo>
+                                                                                <m:mi>P</m:mi>
+                                                                                <m:mo>:</m:mo>
+                                                                                <m:mrow helm:xref="i6">
+                                                                                    <m:mo>Prop</m:mo>
+                                                                                </m:mrow>
+                                                                            </m:mtd>
+                                                                        </m:mtr>
+                                                                        <m:mtr>
+                                                                            <m:mtd>
+                                                                                <m:mrow>
+                                                                                    <m:mo>.</m:mo>
+                                                                                    <m:mrow helm:xref="i7">
+                                                                                        <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                                                            <m:mtr>
+                                                                                                <m:mtd>
+                                                                                                    <m:mo color="Red">&#955;</m:mo>
+                                                                                                    <m:mi>f</m:mi>
+                                                                                                    <m:mo>:</m:mo>
+                                                                                                    <m:mrow helm:xref="i8">
+                                                                                                        <m:mo stretchy="false">(</m:mo>
+                                                                                                        <m:mi helm:xref="i9">A</m:mi>
+                                                                                                        <m:mo color="Blue">&#8594;</m:mo>
+                                                                                                        <m:mrow helm:xref="i10">
+                                                                                                            <m:mo stretchy="false">(</m:mo>
+                                                                                                            <m:mi helm:xref="i11">B</m:mi>
+                                                                                                            <m:mo color="Blue">&#8594;</m:mo>
+                                                                                                            <m:mi helm:xref="i12">P</m:mi>
+                                                                                                            <m:mo stretchy="false">)</m:mo>
+                                                                                                        </m:mrow>
+                                                                                                        <m:mo stretchy="false">)</m:mo>
+                                                                                                    </m:mrow>
+                                                                                                </m:mtd>
+                                                                                            </m:mtr>
+                                                                                            <m:mtr>
+                                                                                                <m:mtd>
+                                                                                                    <m:mrow>
+                                                                                                        <m:mo>.</m:mo>
+                                                                                                        <m:mrow helm:xref="i13">
+                                                                                                            <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                                                                                <m:mtr>
+                                                                                                                    <m:mtd>
+                                                                                                                        <m:mo color="Red">&#955;</m:mo>
+                                                                                                                        <m:mi>a</m:mi>
+                                                                                                                        <m:mo>:</m:mo>
+                                                                                                                        <m:mrow helm:xref="i14">
+                                                                                                                            <m:mo stretchy="false">(</m:mo>
+                                                                                                                            <m:mi xlink:href="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i15">and</m:mi>
+                                                                                                                            <m:mphantom>
+                                                                                                                                <m:mtext>_</m:mtext>
+                                                                                                                            </m:mphantom>
+                                                                                                                            <m:mi helm:xref="i16">A</m:mi>
+                                                                                                                            <m:mphantom>
+                                                                                                                                <m:mtext>_</m:mtext>
+                                                                                                                            </m:mphantom>
+                                                                                                                            <m:mi helm:xref="i17">B</m:mi>
+                                                                                                                            <m:mo stretchy="false">)</m:mo>
+                                                                                                                        </m:mrow>
+                                                                                                                    </m:mtd>
+                                                                                                                </m:mtr>
+                                                                                                                <m:mtr>
+                                                                                                                    <m:mtd>
+                                                                                                                        <m:mrow>
+                                                                                                                            <m:mo>.</m:mo>
+                                                                                                                            <m:mrow helm:xref="i18">
+                                                                                                                                <m:mo>&lt;</m:mo>
+                                                                                                                                <m:mi helm:xref="i19">P</m:mi>
+                                                                                                                                <m:mo>&gt;</m:mo>
+                                                                                                                                <m:mo>CASES</m:mo>
+                                                                                                                                <m:mphantom>
+                                                                                                                                    <m:mtext>_</m:mtext>
+                                                                                                                                </m:mphantom>
+                                                                                                                                <m:mi helm:xref="i20">a</m:mi>
+                                                                                                                                <m:mphantom>
+                                                                                                                                    <m:mtext>_</m:mtext>
+                                                                                                                                </m:mphantom>
+                                                                                                                                <m:mo>OF</m:mo>
+                                                                                                                                <m:mrow>
+                                                                                                                                    <m:mo stretchy="false">(</m:mo>
+                                                                                                                                    <m:mi>conj</m:mi>
+                                                                                                                                    <m:mphantom>
+                                                                                                                                        <m:mtext>_</m:mtext>
+                                                                                                                                    </m:mphantom>
+                                                                                                                                    <m:mi>$1</m:mi>
+                                                                                                                                    <m:mphantom>
+                                                                                                                                        <m:mtext>_</m:mtext>
+                                                                                                                                    </m:mphantom>
+                                                                                                                                    <m:mi>$2</m:mi>
+                                                                                                                                    <m:mo stretchy="false">)</m:mo>
+                                                                                                                                </m:mrow>
+                                                                                                                                <m:mo color="Green">&#8658;</m:mo>
+                                                                                                                                <m:mrow>
+                                                                                                                                    <m:mo stretchy="false">(</m:mo>
+                                                                                                                                    <m:mi helm:xref="i21">f</m:mi>
+                                                                                                                                    <m:mphantom>
+                                                                                                                                        <m:mtext>_</m:mtext>
+                                                                                                                                    </m:mphantom>
+                                                                                                                                    <m:mi>$1</m:mi>
+                                                                                                                                    <m:mphantom>
+                                                                                                                                        <m:mtext>_</m:mtext>
+                                                                                                                                    </m:mphantom>
+                                                                                                                                    <m:mi>$2</m:mi>
+                                                                                                                                    <m:mo stretchy="false">)</m:mo>
+                                                                                                                                </m:mrow>
+                                                                                                                                <m:mphantom>
+                                                                                                                                    <m:mtext>_</m:mtext>
+                                                                                                                                </m:mphantom>
+                                                                                                                                <m:mo>END</m:mo>
+                                                                                                                            </m:mrow>
+                                                                                                                        </m:mrow>
+                                                                                                                    </m:mtd>
+                                                                                                                </m:mtr>
+                                                                                                            </m:mtable>
+                                                                                                        </m:mrow>
+                                                                                                    </m:mrow>
+                                                                                                </m:mtd>
+                                                                                            </m:mtr>
+                                                                                        </m:mtable>
+                                                                                    </m:mrow>
+                                                                                </m:mrow>
+                                                                            </m:mtd>
+                                                                        </m:mtr>
+                                                                    </m:mtable>
+                                                                </m:mrow>
+                                                            </m:mrow>
+                                                        </m:mtd>
+                                                    </m:mtr>
+                                                </m:mtable>
+                                            </m:mrow>
+                                        </m:mrow>
+                                    </m:mtd>
+                                </m:mtr>
+                            </m:mtable>
+                        </m:mrow>
+                        <m:annotation-xml encoding="MathML">
+                            <m:lambda helm:xref="i1">
+                                <m:bvar>
+                                    <m:ci>A</m:ci>
+                                    <m:type>
+                                        <m:apply helm:xref="i2">
+                                            <m:csymbol>Prop</m:csymbol>
+                                        </m:apply>
+                                    </m:type>
+                                </m:bvar>
+                                <m:lambda helm:xref="i3">
+                                    <m:bvar>
+                                        <m:ci>B</m:ci>
+                                        <m:type>
+                                            <m:apply helm:xref="i4">
+                                                <m:csymbol>Prop</m:csymbol>
+                                            </m:apply>
+                                        </m:type>
+                                    </m:bvar>
+                                    <m:lambda helm:xref="i5">
+                                        <m:bvar>
+                                            <m:ci>P</m:ci>
+                                            <m:type>
+                                                <m:apply helm:xref="i6">
+                                                    <m:csymbol>Prop</m:csymbol>
+                                                </m:apply>
+                                            </m:type>
+                                        </m:bvar>
+                                        <m:lambda helm:xref="i7">
+                                            <m:bvar>
+                                                <m:ci>f</m:ci>
+                                                <m:type>
+                                                    <m:apply helm:xref="i8">
+                                                        <m:csymbol>arrow</m:csymbol>
+                                                        <m:ci helm:xref="i9">A</m:ci>
+                                                        <m:apply helm:xref="i10">
+                                                            <m:csymbol>arrow</m:csymbol>
+                                                            <m:ci helm:xref="i11">B</m:ci>
+                                                            <m:ci helm:xref="i12">P</m:ci>
+                                                        </m:apply>
+                                                    </m:apply>
+                                                </m:type>
+                                            </m:bvar>
+                                            <m:lambda helm:xref="i13">
+                                                <m:bvar>
+                                                    <m:ci>a</m:ci>
+                                                    <m:type>
+                                                        <m:apply helm:xref="i14">
+                                                            <m:csymbol>app</m:csymbol>
+                                                            <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i15">and</m:ci>
+                                                            <m:ci helm:xref="i16">A</m:ci>
+                                                            <m:ci helm:xref="i17">B</m:ci>
+                                                        </m:apply>
+                                                    </m:type>
+                                                </m:bvar>
+                                                <m:apply helm:xref="i18">
+                                                    <m:csymbol>mutcase</m:csymbol>
+                                                    <m:ci helm:xref="i19">P</m:ci>
+                                                    <m:ci helm:xref="i20">a</m:ci>
+                                                    <m:apply>
+                                                        <m:csymbol>app</m:csymbol>
+                                                        <m:ci>conj</m:ci>
+                                                        <m:ci>$1</m:ci>
+                                                        <m:ci>$2</m:ci>
+                                                    </m:apply>
+                                                    <m:apply>
+                                                        <m:csymbol>app</m:csymbol>
+                                                        <m:ci helm:xref="i21">f</m:ci>
+                                                        <m:ci>$1</m:ci>
+                                                        <m:ci>$2</m:ci>
+                                                    </m:apply>
+                                                </m:apply>
+                                            </m:lambda>
+                                        </m:lambda>
+                                    </m:lambda>
+                                </m:lambda>
+                            </m:lambda>
+                        </m:annotation-xml>
+                    </m:semantics>
+                </m:mrow>
+            </m:mtd>
+        </m:mtr>
+    </m:mtable>
+</m:math>