]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/cic2acic.ml
NameExpected exception removed. The "identifier" __n is now returned
[helm.git] / helm / ocaml / cic_omdoc / cic2acic.ml
index d8a4421734e24c0b6d0410f6245d6feb6091b751..f7c2317ba660985d0d44285fe12e750b7a002e50 100644 (file)
@@ -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