Added method AndInd.

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 0933dbc4b88a573f09a30f1060e3bc14dadc1859..0295daac326659968bb6d8637ad9956583e90afa 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -699,8 +699,9 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
       if n<0 then raise NotApplicable
       else 
         let method_name =
-          if uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" then
-            "Exists"
+          if (uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" or
+              uri_str = "cic:/Coq/Init/Logic/ex_ind.con") then "Exists"
+          else if uri_str = "cic:/Coq/Init/Logic/and_ind.con" then "AndInd"
           else "ByInduction" in
         let prefix = String.sub uri_str 0 n in
         let ind_str = (prefix ^ ".ind") in 

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 04be41c45cd3515f78f4e83781e3d896d14f0211..575bb687af1eea1966a5aa59138b26afacc06e45 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -192,7 +192,7 @@ let rec justification term2pres p =
       make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in
     P.Mrow([],
       P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"])::
-      P.Mo([],"(")::pres_args@[P.Mo([],")")]) 
+      P.Mtext([],"(")::pres_args@[P.Mtext([],")")]) 
   else proof2pres term2pres p 
      
 and proof2pres term2pres p =
@@ -342,7 +342,10 @@ and proof2pres term2pres p =
             make_concl "that is equivalent to" concl
           else  
             let conclude_body = conclude_aux conclude in
-            let ann_concl = make_concl "we conclude" concl in
+            let ann_concl = 
+              if conclude.Con.conclude_method = "TD_Conversion" then
+                 make_concl "that is equivalent to" concl 
+              else make_concl "we conclude" concl in
             P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
               None,"columnalign","left"],
                 [P.Mtr ([],[P.Mtd ([],conclude_body)]);
@@ -415,6 +418,8 @@ and proof2pres term2pres p =
       byinduction conclude
     else if (conclude.Con.conclude_method = "Exists") then
       exists conclude
+    else if (conclude.Con.conclude_method = "AndInd") then
+      andind conclude
     else if (conclude.Con.conclude_method = "Rewrite") then
       let justif = 
         (match (List.nth conclude.Con.conclude_args 6) with
@@ -645,6 +650,65 @@ and proof2pres term2pres p =
               [P.Mtr([],[P.Mtd([],presacontext)])])
        | _ -> assert false 
 
+     and andind conclude =
+       let module P = Mpresentation in
+       let module Con = Content in
+       let proof_conclusion = 
+         (match conclude.Con.conclude_conclusion with
+            None -> P.Mtext([],"No conclusion???")
+          | Some t -> term2pres t) in
+       let proof,case_arg = 
+         (match conclude.Con.conclude_args with
+             [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg
+           | _ -> assert false;
+             (* 
+             List.map (ContentPp.parg 0) conclude.Con.conclude_args;
+             assert false *)) in
+       let arg = 
+         (match case_arg with
+             Con.Aux n -> assert false
+           | Con.Premise prem ->
+              (match prem.Con.premise_binder with
+                 None -> []
+               | Some n -> [P.Mtext([],"by");P.smallskip;P.Mi([],n)])
+           | Con.Lemma lemma -> 
+               [P.Mtext([],"by");P.smallskip;P.Mi([],lemma.Con.lemma_name)]
+           | _ -> assert false) in
+       match proof.Con.proof_context with
+         `Hypothesis hyp1::`Hypothesis hyp2::tl ->
+            let get_name hyp =
+              (match hyp.Con.dec_name with
+                None -> "_"
+              | Some s -> s) in
+            let preshyp1 = 
+              P.Mrow ([],
+               [P.Mtext([],"(");
+                P.Mi([],get_name hyp1);
+                P.Mtext([],")");
+                P.smallskip;
+                term2pres hyp1.Con.dec_type]) in
+            let preshyp2 = 
+              P.Mrow ([],
+               [P.Mtext([],"(");
+                P.Mi([],get_name hyp2);
+                P.Mtext([],")");
+                P.smallskip;
+                term2pres hyp2.Con.dec_type]) in
+            (* let body = proof2pres {proof with Con.proof_context = tl} in *)
+            let body = conclude2pres proof.Con.proof_conclude false true in
+            let presacontext = 
+              acontext2pres proof.Con.proof_apply_context body false in
+            P.Mtable 
+              ([None,"align","baseline 1"; None,"equalrows","false"; 
+                None,"columnalign","left"],
+               [P.Mtr ([],[P.Mtd ([],
+                 P.Mrow([],arg@[P.smallskip;P.Mtext([],"we have")]))]);
+                P.Mtr ([],[P.Mtd ([],preshyp1)]);
+                P.Mtr ([],[P.Mtd ([],P.Mtext([],"and"))]);
+                P.Mtr ([],[P.Mtd ([],preshyp2)]);
+                P.Mtr ([],[P.Mtd ([],presacontext)])]);
+         | _ -> assert false
+
      and exists conclude =
        let module P = Mpresentation in
        let module Con = Content in

diff --git a/helm/ocaml/cic_transformations/mpresentation.ml b/helm/ocaml/cic_transformations/mpresentation.ml
index 34c65a4174e561f8fd42e9991b4588492f5e1360..3c4f929024b080b311b2abd36898768e3946ec58 100644 (file)
--- a/helm/ocaml/cic_transformations/mpresentation.ml
+++ b/helm/ocaml/cic_transformations/mpresentation.ml
@@ -207,7 +207,7 @@ and print_mrow =
 and print_mtd =
   let module X = Xml in
   function 
-     Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr (print_mpres m)
+     Mtd (attr,m) -> X.xml_nempty ~prefix "mtd" attr [< (print_mpres m) ; X.xml_nempty ~prefix "mphantom" [] (X.xml_nempty ~prefix "mtext" [] (X.xml_cdata "(")) >]
 ;;
 
 let print_mpres pres =
@@ -217,7 +217,7 @@ let print_mpres pres =
      [Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ;
       Some "xmlns","helm","http://www.cs.unibo.it/helm" ;
       Some "xmlns","xlink","http://www.w3.org/1999/xlink"
-     ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"] (print_mpres pres))
+     ] (Xml.xml_nempty ~prefix "mstyle" [None, "mathvariant", "normal"; None, "rowspacing", "0.6ex"] (print_mpres pres))
  >]