[arg] -> idref (k ~context arg)
| _ -> idref (Ast.Appl (List.map (k ~context) args))))
| NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
+ (try
let name = NUri.name_of_uri uri in
(* CSC
let uri_str = UriManager.string_of_uri uri in
| `Term -> Some case_indty
in
idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns))
+ with
+ NCicEnvironment.ObjectNotFound msg ->
+ idref (Ast.Case(k ~context te,Some ("NOT_FOUND: " ^ Lazy.force msg,None),
+ Some (k ~context outty),
+ (List.map (fun t -> Ast.Pattern ("????", None, []), k ~context t)
+ patterns))))
;;
let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
n, is_ind, ty, List.map (build_constractor lno context) cl
in
match kind with
- | NCic.Constant (_, n, xbo, ty, (_, flavour, pragma)) ->
+ | NCic.Constant (_, n, xbo, ty, attrs) ->
let ty = nast_of_cic ~context:[] ty in
let xbo = match xbo with
| Some bo -> Some (nast_of_cic ~context:[] bo)
| None -> None
in
- N.Theorem (flavour, n, ty, xbo, pragma)
- | NCic.Inductive (is_ind, lno, itl, (_, `Regular)) ->
+ N.Theorem (n, ty, xbo, attrs)
+ | NCic.Inductive (is_ind, lno, itl, (src, `Regular)) ->
let captures, context = build_captures lno itl in
- N.Inductive (captures, List.map (build_inductive is_ind lno context) itl)
+ N.Inductive (captures, List.map (build_inductive is_ind lno context) itl, src)
| _ -> assert false (* NCic.Fixpoint (is_rec, ifl, _) -> *)
let nmap_obj status = with_idrefs nmap_obj0 status