bumped version (tag soon)

[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 d8a4421734e24c0b6d0410f6245d6feb6091b751..8418a64d42506796fc8afb5d245e12415c7c7869 100644 (file)
--- 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