-let r2s pp_fix_name r =
- try
- match r with
- | NReference.Ref (u,NReference.Ind (_,i,_)) ->
- (match NCicLibrary.get_obj u with
- | _,_,_,_, NCic.Inductive (_,_,itl,_) ->
- let _,name,_,_ = List.nth itl i in name
- | _ -> assert false)
- | NReference.Ref (u,NReference.Con (i,j,_)) ->
- (match NCicLibrary.get_obj u with
- | _,_,_,_, NCic.Inductive (_,_,itl,_) ->
- let _,_,_,cl = List.nth itl i in
- let _,name,_ = List.nth cl (j-1) in name
- | _ -> assert false)
- | NReference.Ref (u,(NReference.Decl | NReference.Def _)) ->
- (match NCicLibrary.get_obj u with
- | _,_,_,_, NCic.Constant (_,name,_,_,_) -> name
- | _ -> assert false)
- | NReference.Ref (u,(NReference.Fix (i,_,_)|NReference.CoFix i)) ->
- (match NCicLibrary.get_obj u with
- | _,_,_,_, NCic.Fixpoint (_,fl,_) ->
- if pp_fix_name then
- let _,name,_,_,_ = List.nth fl i in name
- else
- NUri.name_of_uri u ^"("^ string_of_int i ^ ")"
- | _ -> assert false)
- with NCicLibrary.ObjectNotFound _ -> NReference.string_of_reference r
-;;
-
-let nast_of_cic ~subst =
- let rec k = function
- | NCic.Rel n -> Ast.Ident ("-" ^ string_of_int n, None)
- | NCic.Const r -> Ast.Ident (r2s true r, None)
+let nast_of_cic ~subst ~context =
+ let rec k ctx = function
+ | NCic.Rel n ->
+ (try
+ let name,_ = List.nth ctx (n-1) in
+ let name = if name = "_" then "__"^string_of_int n else name in
+ Ast.Ident (name,None)
+ with Failure "nth" | Invalid_argument "List.nth" ->
+ Ast.Ident ("-" ^ string_of_int (n - List.length ctx),None))
+ | NCic.Const r -> Ast.Ident (NCicPp.r2s false r, None)