* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let debug_print = fun _ -> ()
let rec higher_name arity =
Cic.Rel n ->
(match List.nth context (n-1) with
None -> assert false
- | Some (Cic.Anonymous,_) -> assert false
+ | Some (Cic.Anonymous,_) -> "eccomi_qua"
| Some (Cic.Name s,_) -> get_initial s)
| Cic.Var (uri,_) -> get_initial (UriManager.name_of_uri uri)
| Cic.Sort _ -> higher_name 0 ty
C.Anonymous ->
if List.mem k rels2 then
(
- debug_print "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name" ;
+ debug_print (lazy "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name") ;
C.Anonymous
)
else