let debug_print s = prerr_endline (Lazy.force s);;
let debug_print _ = ();;
+let reference_of_oxuri = ref (fun _ -> assert false);;
+let set_reference_of_oxuri f = reference_of_oxuri := f;;
+
let cic_name_of_name = function
| Ast.Ident (n, None) -> n
| _ -> assert false
| CicNotationPt.Uri (uri, subst) ->
assert (subst = None);
(try
- NCic.Const (OCic2NCic.reference_of_oxuri(UriManager.uri_of_string uri))
+ NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri))
with NRef.IllFormedReference _ ->
CicNotationPt.fail loc "Ill formed reference")
| CicNotationPt.NRef nref -> NCic.Const nref
+ | 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
interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
let uri = match uri with | None -> assert false | Some u -> u in
match obj with
- | CicNotationPt.Theorem (flavour, name, ty, bo) ->
+ | CicNotationPt.Theorem (flavour, name, ty, bo, pragma) ->
let ty' =
interpretate_term
~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty
uri, height, [], [],
(match bo,flavour with
| None,`Axiom ->
- let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+ let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
NCic.Constant ([],name,None,ty',attrs)
| Some _,`Axiom -> assert false
| None,_ ->
- let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+ let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
| Some bo,_ ->
(match bo with
([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
defs
in
- let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+ let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
NCic.Fixpoint (inductive,inductiveFuns,attrs)
| bo ->
let bo =
interpretate_term
~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
in
- let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+ let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
NCic.Constant ([],name,Some bo,ty',attrs)))
| CicNotationPt.Inductive (params,tyl) ->
let context,params =
;;
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)