X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.ml;h=81cfaaf099e7290d52a37ddccb2724c4defa92ea;hb=13d6baa55139729871604c0c3f70a70077ba85ca;hp=4c7b955c9a22962cb6465eb3c9cbfcea979cad0f;hpb=081cb0ae54c7e5babdedeea7559d667183a38638;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 4c7b955c9..81cfaaf09 100644
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -408,7 +408,7 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
     let ids_to_hypotheses = Hashtbl.create 23 in
     let hypotheses_seed = ref 0 in
     let seed = ref 1 in (* 'i0' is used for the whole sequent *)
-    let sequent =
+    let unsh_sequent =
      let i,canonical_context,term = sequent in
       let canonical_context' =
        List.fold_right
@@ -432,9 +432,10 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
     let (metano,acontext,agoal) = 
       aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids 
       ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
-      metasenv sequent in
-    ("i0",metano,acontext,agoal), 
-     ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses
+      metasenv unsh_sequent in
+    (unsh_sequent,
+     (("i0",metano,acontext,agoal), 
+      ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
 ;;
 
 let acic_object_of_cic_object ?(eta_fix=true) obj =