aux 1 context
let interpretate_term_and_interpretate_term_option (status: #NCic.status)
- ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~uri ~is_path
+ ~create_dummy_ids ~obj_context ~mk_choice ~env ~uri ~is_path
~localization_tbl
=
(* create_dummy_ids shouldbe used only for interpretating patterns *)
"branch pattern must be \"_\"")))
) branches in
let indtype_ref =
- NReference.reference_of_string "cic:/fake_indty.ind(0,0,0)"
+ let uri = NUri.uri_of_string "cic:/matita/dummy/indty.ind" in
+ NRef.reference_of_spec uri (NRef.Ind (true,1,1))
in
NCic.Match (indtype_ref, cic_outtype, cic_term,
(List.map do_branch branches))
| Some (indty_ident, _) ->
(match Disambiguate.resolve ~env ~mk_choice
(DT.Id indty_ident) (`Args []) with
- | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
+ | NCic.Const (NRef.Ref (_,NRef.Ind _) as r) -> r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
(lazy "The type of the term to be matched is still unknown"))
*)
(match Disambiguate.resolve ~env ~mk_choice
(DT.Id (fst_constructor branches)) (`Args []) with
- | NCic.Const (NReference.Ref (_,NReference.Con _) as r) ->
+ | NCic.Const (NRef.Ref (_,NRef.Con _) as r) ->
let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in
- NReference.mk_indty b r
+ NRef.mk_indty b r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
(lazy "The type of the term to be matched is still unknown"))
| NotationPt.Uri (uri, subst) ->
assert (subst = None);
(try
- NCic.Const (NReference.reference_of_string uri)
+ NCic.Const (NRef.reference_of_string uri)
with NRef.IllFormedReference _ ->
NotationPt.fail loc "Ill formed reference")
| NotationPt.NRef nref -> NCic.Const nref
List.fold_left
(fun (i,res) (name,_,_,_) ->
let nref =
- NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno))
+ NRef.reference_of_spec uri (NRef.Ind (inductive,i,leftno))
in
i+1,(name,nref)::res)
(0,[]) tyl) in
(interpretate_term status ~obj_context:[] ~context ~env ~uri:None
~is_path:false ty) in
let nref =
- NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
+ NRef.reference_of_spec uri (NRef.Ind (true,0,leftno)) in
let obj_context = [name,nref] in
let fields' =
snd (
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))
+ (ncic_name_of_ident name, NRef.reference_of_spec uri
+ (if inductive then NRef.Fix (i,k,0)
+ else NRef.CoFix i)) :: acc))
(0,[]) defs
in
let inductiveFuns =
~universe ~uri:None ~pp_thing:(NotationPp.pp_term status)
~passes:(MultiPassDisambiguator.passes ())
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
- ~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
+ ~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice ?create_dummy_ids:None)
~refine_thing:(refine_term status) (text,prefix_len,term)
~mk_localization_tbl ~expty ~subst
in