NameExpected exception removed. The "identifier" __n is now returned

(as CicPp does).

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index d8a4421734e24c0b6d0410f6245d6feb6091b751..f7c2317ba660985d0d44285fe12e750b7a002e50 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

diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli
index 4f686da443ef71b1cc2a4a869aa855f4b3a71a80..9cef0cb38155a164403d1f909b2dd6970088336e 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.mli
+++ b/helm/ocaml/cic_omdoc/cic2acic.mli
@@ -24,7 +24,6 @@
  *)
 
 exception NotEnoughElements
-exception NameExpected
 
 val source_id_of_id : string -> string