Unuseful id removed from hypothesis.

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

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