Few modif in eta-fixing.

[helm.git] / helm / ocaml / cic_omdoc / cic2content.ml

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 21b39fe65209372c21cd6078fe205ce33084d18b..0933dbc4b88a573f09a30f1060e3bc14dadc1859 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -257,10 +257,10 @@ let generate_conversion seed top_down id inner_proof ~ids_to_inner_types =
               };
           }
         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;
@@ -436,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
 
@@ -500,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
@@ -686,6 +698,10 @@ 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" then
+            "Exists"
+          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
@@ -700,7 +716,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
@@ -767,14 +786,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))
@@ -819,7 +838,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;