X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=0295daac326659968bb6d8637ad9956583e90afa;hb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;hp=0e0edf100066ec9ceaa616f001092972ca392ae7;hpb=414dc18cdbc1f431758cfce79b0b7827e2419d39;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 0e0edf100..0295daac3 100644
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -243,7 +243,7 @@ let generate_conversion seed top_down id inner_proof ~ids_to_inner_types =
      None -> inner_proof
    | Some expty ->
        if inner_proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
-         { K.proof_name = None ;
+         { K.proof_name = inner_proof.K.proof_name;
             K.proof_id   = gen_id seed;
             K.proof_context = [] ;
             K.proof_apply_context = [];
@@ -251,15 +251,16 @@ let generate_conversion seed top_down id inner_proof ~ids_to_inner_types =
               { K.conclude_id = gen_id seed; 
                 K.conclude_aref = id;
                 K.conclude_method = "TD_Conversion";
-                K.conclude_args = [K.ArgProof inner_proof];
+                K.conclude_args = 
+                  [K.ArgProof {inner_proof with K.proof_name = None}];
                 K.conclude_conclusion = Some expty
               };
           }
         else
-          { K.proof_name = None ;
+          { K.proof_name =  inner_proof.K.proof_name;
             K.proof_id   = gen_id seed;
             K.proof_context = [] ;
-            K.proof_apply_context = [inner_proof];
+            K.proof_apply_context = [{inner_proof with K.proof_name = None}];
             K.proof_conclude = 
               { K.conclude_id = gen_id seed; 
                 K.conclude_aref = id;
@@ -435,15 +436,27 @@ build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
  let module K = Content in
   try
    let sort = Hashtbl.find ids_to_inner_sorts id in
+   (match name_of n with
+     Some "w" -> prerr_endline ("build_def: " ^ sort );
+   | _ -> ());
    if sort = "Prop" then
-      `Proof (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
+       (prerr_endline ("entro");
+       let p = 
+        (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
+       in 
+        (match p.K.proof_name with
+           Some "w" -> prerr_endline ("TUTTO BENE:");
+         | Some s -> prerr_endline ("mi chiamo " ^ s);
+         | _ -> prerr_endline ("ho perso il nome"););
+      prerr_endline ("esco"); `Proof p;)
    else 
+      (prerr_endline ("siamo qui???");
       `Definition
         { K.def_name = name_of n;
           K.def_id = gen_id seed; 
           K.def_aref = id;
           K.def_term = t
-        }
+        })
   with
    Not_found -> assert false
 
@@ -499,7 +512,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
         else raise Not_a_proof 
     | C.ALetIn (id,n,s,t) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-        if sort = "Prop" then 
+        if sort = "Prop" then
           let proof = aux t in
           let proof' = 
             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
@@ -685,6 +698,11 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                with Not_found -> -1) in
       if n<0 then raise NotApplicable
       else 
+        let method_name =
+          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 
         let ind_uri = UriManager.uri_of_string ind_str in
@@ -699,7 +717,10 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
           if n = 0 then ([],l) else
           let p,a = split (n-1) (List.tl l) in
           ((List.hd l::p),a) in
-        let params_and_IP,tail_args = split (noparams+1) args in 
+        let params_and_IP,tail_args = split (noparams+1) args in
+        if method_name = "Exists" then
+          (prerr_endline ("+++++args++++:" ^ string_of_int (List.length args));
+           prerr_endline ("+++++tail++++:" ^ string_of_int (List.length tail_args)));
         let constructors = 
             (match inductive_types with
               [(_,_,_,l)] -> l
@@ -766,14 +787,14 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                   hdarg::(build_method_args (tlc,tla))
               | _ -> assert false in
           build_method_args (constructors1,args_for_cases) in
-          { K.proof_name = None;
+          { K.proof_name = name;
             K.proof_id   = gen_id seed;
             K.proof_context = []; 
             K.proof_apply_context = serialize seed subproofs;
             K.proof_conclude = 
               { K.conclude_id = gen_id seed; 
                 K.conclude_aref = id;
-                K.conclude_method = "ByInduction";
+                K.conclude_method = method_name;
                 K.conclude_args =
                   K.Aux (string_of_int no_constructors) 
                   ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
@@ -818,7 +839,7 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                     else K.Term a in
                 hd::(ma_aux (n-1) tl) in
           (ma_aux 3 args) in 
-          { K.proof_name = None;
+          { K.proof_name = name;
             K.proof_id   = gen_id seed;
             K.proof_context = []; 
             K.proof_apply_context = serialize seed subproofs;