- (match bo with
- | NotationPt.LetRec (kind, defs, _) ->
- let inductive = kind = `Inductive in
- let _,obj_context =
- List.fold_left
- (fun (i,acc) (_,(name,_),_,k) ->
- (i+1,
- (ncic_name_of_ident name, NReference.reference_of_spec uri
- (if inductive then NReference.Fix (i,k,0)
- else NReference.CoFix i)) :: acc))
- (0,[]) defs
- in
- let inductiveFuns =
- List.map
- (fun (params, (name, typ), body, decr_idx) ->
- let add_binders kind t =
- List.fold_right
- (fun var t ->
- NotationPt.Binder (kind, var, t)) params t
- in
- let cic_body =
- interpretate_term
- ~obj_context ~context ~env ~uri:None ~is_path:false
- (add_binders `Lambda body)
- in
- let cic_type =
- interpretate_term_option
- ~obj_context:[]
- ~context ~env ~uri:None ~is_path:false `Type
- (HExtlib.map_option (add_binders `Pi) typ)
- in
- ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
- defs
- in
- let attrs = `Provided, flavour, pragma in
- NCic.Fixpoint (inductive,inductiveFuns,attrs)
- | bo ->
- let bo =
- interpretate_term
- ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
- in
- let attrs = `Provided, flavour, pragma in
- NCic.Constant ([],name,Some bo,ty',attrs)))