let aliases =
List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
status#disambiguate_db.aliases new_aliases in
let aliases =
List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
status#disambiguate_db.aliases new_aliases in
=
let diff, metasenv, subst, cic =
singleton "first"
(NCicDisambiguate.disambiguate_term
=
let diff, metasenv, subst, cic =
singleton "first"
(NCicDisambiguate.disambiguate_term
~mk_implicit ~fix_instance
~description_of_alias:GrafiteAst.description_of_alias
~context ~metasenv ~subst thing)
in
~mk_implicit ~fix_instance
~description_of_alias:GrafiteAst.description_of_alias
~context ~metasenv ~subst thing)
in
- metasenv, subst, estatus, cic
+ metasenv, subst, status, cic
NotationPt.term Disambiguate.disambiguator_input option *
(string * NCic.term) list * NCic.term option
NotationPt.term Disambiguate.disambiguator_input option *
(string * NCic.term) list * NCic.term option
-let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
- let interp path = NCicDisambiguate.disambiguate_path path in
+let disambiguate_npattern status (text, prefix_len, (wanted, hyp_paths, goal_path)) =
+ let interp path = NCicDisambiguate.disambiguate_path status path in
let goal_path = HExtlib.map_option interp goal_path in
let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
let goal_path = HExtlib.map_option interp goal_path in
let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
match obj with
| NotationPt.Inductive (_,(name,_,_,_)::_)
| NotationPt.Record (_,name,_,_) -> name ^ ".ind"
match obj with
| NotationPt.Inductive (_,(name,_,_,_)::_)
| NotationPt.Record (_,name,_,_) -> name ^ ".ind"
- | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
+ | NotationPt.Theorem (name,_,_,_) -> name ^ ".con"
- ~mk_choice:(ncic_mk_choice estatus)
- ~mk_implicit ~fix_instance
- ~uri
- ~rdb:estatus
- ~aliases:estatus#disambiguate_db.aliases
- ~universe:(Some estatus#disambiguate_db.multi_aliases)
+ ~mk_choice:(ncic_mk_choice status)
+ ~mk_implicit ~fix_instance ~uri
+ ~aliases:status#disambiguate_db.aliases
+ ~universe:(Some status#disambiguate_db.multi_aliases)
DisambiguateTypes.Id name,
GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
) references) refs)
DisambiguateTypes.Id name,
GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
) references) refs)