Unuseful id removed from hypothesis.

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index b8679dc62e0b32df9beea1added139d870af5a7b..c0e514d37406835bc6f7f224806fe2ac1fc60cdd 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -63,9 +63,11 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
  let module T = CicTypeChecker in
  let module C = Cic in
   let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in
+prerr_endline "*************** INIZIO DOUBLE TYPE INFERENCE ************";
    let terms_to_types =
     D.double_type_of metasenv context t expectedty
    in
+prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
     let rec aux computeinnertypes father context idrefs tt =
      let fresh_id'' = fresh_id' father tt in
      (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
@@ -339,6 +341,7 @@ let acic_object_of_cic_object obj =
         C.AVariable
          ("mettereaposto",id,abo,aty, params)
     | C.CurrentProof (id,conjectures,bo,ty,params) ->
+prerr_endline "************* INIZIO ETA_FIXING (congetture) ********" ;
        let conjectures' =
         List.map
          (function (i,canonical_context,term) ->
@@ -354,6 +357,7 @@ let acic_object_of_cic_object obj =
             (i,canonical_context',term')
          ) conjectures
        in
+prerr_endline "************* INIZIO CIC ==> ACIC (congetture) ********" ;
        let aconjectures =
         List.map
          (function (i,canonical_context,term) as conjecture ->
@@ -400,8 +404,10 @@ let acic_object_of_cic_object obj =
              in
               (cid,i,(List.rev revacanonical_context),aterm)
          ) conjectures' in
+prerr_endline "*********** INIZIO ETA FIXING PROVA **********";
        let bo' = E.eta_fix conjectures' bo in
        let ty' = E.eta_fix conjectures' ty in
+prerr_endline "*********** INIZIO CIC ==> ACIC PROVA **********";
        let abo =
         acic_term_of_cic_term_context' conjectures' [] [] bo' (Some ty') in
        let aty = acic_term_of_cic_term_context' conjectures' [] [] ty' None in

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 58ef34c871cd49cdc43c2302e73e4fa321c17ebf..0f23afb5691b7721b0b67b2f9e73ce267d3a9147 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -834,30 +834,28 @@ let map_conjectures
  let context' =
   List.map
    (function
-       (id,None) as item -> item
+       (id,None) -> None
      | (id,Some (name,Cic.ADecl t)) ->
-         id,
-          Some
-           (* We should call build_decl_item, but we have not computed *)
-           (* the inner-types ==> we always produce a declaration      *)
-           (`Declaration
-             { K.dec_name = name_of name;
-               K.dec_id = gen_id declaration_prefix seed; 
-               K.dec_inductive = false;
-               K.dec_aref = get_id t;
-               K.dec_type = t
-             })
+         Some
+          (* We should call build_decl_item, but we have not computed *)
+          (* the inner-types ==> we always produce a declaration      *)
+          (`Declaration
+            { K.dec_name = name_of name;
+              K.dec_id = gen_id declaration_prefix seed; 
+              K.dec_inductive = false;
+              K.dec_aref = get_id t;
+              K.dec_type = t
+            })
      | (id,Some (name,Cic.ADef t)) ->
-         id,
-          Some
-           (* We should call build_def_item, but we have not computed *)
-           (* the inner-types ==> we always produce a declaration     *)
-           (`Definition
-              { K.def_name = name_of name;
-                K.def_id = gen_id definition_prefix seed; 
-                K.def_aref = get_id t;
-                K.def_term = t
-              })
+         Some
+          (* We should call build_def_item, but we have not computed *)
+          (* the inner-types ==> we always produce a declaration     *)
+          (`Definition
+             { K.def_name = name_of name;
+               K.def_id = gen_id definition_prefix seed; 
+               K.def_aref = get_id t;
+               K.def_term = t
+             })
    ) context
  in
   (id,n,context',ty)

diff --git a/helm/ocaml/cic_omdoc/content.ml b/helm/ocaml/cic_omdoc/content.ml
index c3c2295ca3703370079e6145042eafafdec80484..6679cfabb466e35758710a6edeba0f542e9448fa 100644 (file)
--- a/helm/ocaml/cic_omdoc/content.ml
+++ b/helm/ocaml/cic_omdoc/content.ml
@@ -148,7 +148,6 @@ type 'term conjecture = id * int * 'term context * 'term
 and 'term context = 'term hypothesis list
 
 and 'term hypothesis =
- id *
  ['term decl_context_element | ('term,'term proof) def_context_element ] option
 ;;
 

diff --git a/helm/ocaml/cic_omdoc/content.mli b/helm/ocaml/cic_omdoc/content.mli
index a672cd83cffb8c6176f70511ba6b34c06b5c46fc..fea233da0d2d321511db9a8d74d46a018e339faa 100644 (file)
--- a/helm/ocaml/cic_omdoc/content.mli
+++ b/helm/ocaml/cic_omdoc/content.mli
@@ -138,7 +138,6 @@ type 'term conjecture = id * int * 'term context * 'term
 and 'term context = 'term hypothesis list
 
 and 'term hypothesis =
- id *
  ['term decl_context_element | ('term,'term proof) def_context_element ] option
 ;;
 

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index 644f55920bd76e72ebb9529ee62ba54a9e0b658e..29e81bffb813dd3122ee097d1f9b05437e430646 100644 (file)
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -238,19 +238,19 @@ let cobj2obj deannotate (id,params,metasenv,obj) =
                let canonical_context' =
                 List.map
                  (function
-                     _,None -> None
-                   | _,Some (`Declaration d) 
-                   | _,Some (`Hypothesis d) ->
+                     None -> None
+                   | Some (`Declaration d) 
+                   | Some (`Hypothesis d) ->
                      (match d with
                         {K.dec_name = Some n ; K.dec_type = t} ->
                           Some (Cic.Name n, Cic.Decl (deannotate t))
                       | _ -> assert false)
-                   | _,Some (`Definition d) ->
+                   | Some (`Definition d) ->
                       (match d with
                           {K.def_name = Some n ; K.def_term = t} ->
                             Some (Cic.Name n, Cic.Def (deannotate t))
                         | _ -> assert false)
-                   | _,Some (`Proof d) ->
+                   | Some (`Proof d) ->
                       (match d with
                           {K.proof_name = Some n } ->
                             Some (Cic.Name n, Cic.Def (proof2cic deannotate d))

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 9a5ad74fd9f6d954eb1202f04ac3b7f75be6fc29..cfa061bfb2e442c93da5457d2fa7545ccf444edc 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -810,13 +810,13 @@ let content2pres term2pres (id,params,metasenv,obj) =
                            (P.Mrow [Some "helm", "xref", id]
                              (List.map
                                (function
-                                   (_,None) ->
+                                   None ->
                                      P.Mrow []
                                       [ P.Mi [] "_" ;
                                         P.Mo [] ":?" ;
                                         P.Mi [] "_"]
-                                 | (_,Some (`Declaration d))
-                                 | (_,Some (`Hypothesis d)) ->
+                                 | Some (`Declaration d)
+                                 | Some (`Hypothesis d) ->
                                     let
                                      { K.dec_name = dec_name ;
                                        K.dec_type = ty } = d
@@ -828,7 +828,7 @@ let content2pres term2pres (id,params,metasenv,obj) =
                                             | Some n -> n) ;
                                          P.Mo [] ":" ;
                                          term2pres ty]
-                                 | (_,Some (`Definition d)) ->
+                                 | Some (`Definition d) ->
                                     let
                                      { K.def_name = def_name ;
                                        K.def_term = bo } = d
@@ -840,7 +840,7 @@ let content2pres term2pres (id,params,metasenv,obj) =
                                             | Some n -> n) ;
                                          P.Mo [] ":=" ;
                                          term2pres bo]
-                                 | (_,Some (`Proof p)) ->
+                                 | Some (`Proof p) ->
                                     let proof_name = p.K.proof_name in
                                      P.Mrow []
                                       [ P.Mi []