X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.ml;h=8418a64d42506796fc8afb5d245e12415c7c7869;hb=b38de2d3fa8bbe346c59c18bbeb889f29e493f63;hp=d8a4421734e24c0b6d0410f6245d6feb6091b751;hpb=2e062d07e358eb95f0dcbec8fcdfbc2a4fb9ae1f;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index d8a442173..8418a64d4 100644
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -64,7 +64,6 @@ let fresh_id seed ids_to_terms ids_to_father_ids =
 let source_id_of_id id = "#source#" ^ id;;
 
 exception NotEnoughElements;;
-exception NameExpected;;
 
 (*CSC: cut&paste da cicPp.ml *)
 (* get_nth l n   returns the nth element of the list l if it exists or *)
@@ -173,7 +172,7 @@ Cic.Sort Cic.Type ;
              let id =
               match get_nth context n with
                  (Some (C.Name s,_)) -> s
-               | _ -> raise NameExpected
+               | _ -> "__" ^ string_of_int n
              in
               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
               if innersort = "Prop"  && expected_available then
@@ -204,7 +203,7 @@ Cic.Sort Cic.Type ;
                   | Some _, None -> assert false (* due to typing rules *))
                 canonical_context l))
           | C.Sort s -> C.ASort (fresh_id'', s)
-          | C.Implicit -> C.AImplicit (fresh_id'')
+          | C.Implicit annotation -> C.AImplicit (fresh_id'', annotation)
           | C.Cast (v,t) ->
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop" then