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 *)
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
| 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