with NRef.IllFormedReference _ ->
CicNotationPt.fail loc "Ill formed reference")
| CicNotationPt.NRef nref -> NCic.Const nref
- | CicNotationPt.NCic t ->
- let context = (* to make metas_of_term happy *)
- List.map (fun x -> x,NCic.Decl (NCic.Implicit `Type)) context in
- assert(NCicUntrusted.metas_of_term [] context t = []); t
+ | CicNotationPt.NCic t -> t
| CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
| CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
| CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
| `MutualDefinition -> `Definition
| `Fact -> `Fact
| `Lemma -> `Lemma
- | `Remark -> `Corollary
+ | `Remark -> `Example
| `Theorem -> `Theorem
| `Variant -> `Corollary
| `Axiom -> `Fact
;;
let disambiguate_term ~context ~metasenv ~subst ~expty
- ~mk_implicit ~description_of_alias ~mk_choice
+ ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
~aliases ~universe ~rdb ~lookup_in_library
(text,prefix_len,term)
=
MultiPassDisambiguator.disambiguate_thing
~freshen_thing:CicNotationUtil.freshen_term
~context ~metasenv ~initial_ugraph:() ~aliases
- ~mk_implicit ~description_of_alias
+ ~mk_implicit ~description_of_alias ~fix_instance
~string_context_of_context:(List.map (fun (x,_) -> Some x))
~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
~passes:(MultiPassDisambiguator.passes ())
;;
let disambiguate_obj
- ~mk_implicit ~description_of_alias ~mk_choice
+ ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
~aliases ~universe ~rdb ~lookup_in_library ~uri
(text,prefix_len,obj)
=
MultiPassDisambiguator.disambiguate_thing
~freshen_thing:CicNotationUtil.freshen_obj
~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
- ~mk_implicit ~description_of_alias
+ ~mk_implicit ~description_of_alias ~fix_instance
~string_context_of_context:(List.map (fun (x,_) -> Some x))
~universe
~uri:(Some uri)