let localise t =
try NCicUntrusted.NCicHash.find localization_tbl t
with Not_found ->
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
- assert false
+ prerr_endline ("NOT LOCALISED" ^ NCicPp.ppterm ~metasenv ~subst ~context t);
+ (*assert false*) HExtlib.dummy_floc
in
let metasenv, subst, term, _ =
NCicRefiner.typeof
;;
let refine_obj
- ~coercion_db metasenv subst context uri
- ~use_coercions obj _ ugraph ~localization_tbl
+ ~coercion_db metasenv subst context _uri
+ ~use_coercions obj _ _ugraph ~localization_tbl
=
assert (metasenv=[]);
assert (subst=[]);
with NRef.IllFormedReference _ ->
CicNotationPt.fail loc "Ill formed reference")
| CicNotationPt.Implicit -> NCic.Implicit `Term
- | CicNotationPt.UserInput -> assert false (*NCic.Implicit (Some `Hole)
-patterns not implemented *)
+ | CicNotationPt.UserInput -> NCic.Implicit `Hole
| CicNotationPt.Num (num, i) ->
Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
| CicNotationPt.Meta (index, subst) ->
~context
;;
+let disambiguate_path path =
+ let localization_tbl = NCicUntrusted.NCicHash.create 23 in
+ fst
+ (interpretate_term_and_interpretate_term_option
+ ~obj_context:[] ~mk_choice:(fun _ -> assert false)
+ ~create_dummy_ids:true ~env:DisambiguateTypes.Environment.empty
+ ~uri:None ~is_path:true ~localization_tbl) ~context:[] path
+;;
+
let new_flavour_of_flavour = function
| `Definition -> `Definition
| `MutualDefinition -> `Definition