[] subst in
[ Node ([loc], Id name, terms) ]))
| Ast.Uri _ -> []
- | Ast.Implicit -> []
+ | Ast.NRef _ -> []
+ | Ast.NCic _ -> []
+ | Ast.Implicit _ -> []
| Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
| Ast.Meta (index, local_context) ->
List.fold_left
let domain_of_obj ~context ast =
assert (context = []);
match ast with
- | Ast.Theorem (_,_,ty,bo) ->
+ | Ast.Theorem (_,_,ty,bo,_) ->
domain_of_term [] ty
@ (match bo with
None -> []
let disambiguate_thing
~context ~metasenv ~subst ~use_coercions
~string_context_of_context
- ~initial_ugraph:base_univ ~hint
+ ~initial_ugraph:base_univ ~expty
~mk_implicit ~description_of_alias
~aliases ~universe ~lookup_in_library
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
interpretate_thing ~context ~env:filled_env
~uri ~is_path:false thing ~localization_tbl
in
- let cic_thing = (fst hint) metasenv cic_thing in
let foo () =
- let k =
refine_thing metasenv subst context uri
- ~use_coercions cic_thing ugraph ~localization_tbl
- in
- let k = (snd hint) k in
- k
+ ~use_coercions cic_thing expty ugraph ~localization_tbl
in refine_profiler.HExtlib.profile foo ()
with
| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))