open Printf
open DisambiguateTypes
-open UriManager
module Ast = NotationPt
module NRef = NReference
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
| NotationPt.Uri (uri, subst) ->
assert (subst = None);
(try
- NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri))
+ NCic.Const (NReference.reference_of_string uri)
with NRef.IllFormedReference _ ->
NotationPt.fail loc "Ill formed reference")
| NotationPt.NRef nref -> NCic.Const nref
- | NotationPt.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
+ | NotationPt.NCic t -> t
| NotationPt.Implicit `Vector -> NCic.Implicit `Vector
| NotationPt.Implicit `JustOne -> NCic.Implicit `Term
| NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
~uri:None ~is_path:true ~localization_tbl) ~context:[] path
;;
-let new_flavour_of_flavour = function
- | `Definition -> `Definition
- | `MutualDefinition -> `Definition
- | `Fact -> `Fact
- | `Lemma -> `Lemma
- | `Remark -> `Example
- | `Theorem -> `Theorem
- | `Variant -> `Corollary
- | `Axiom -> `Fact
-;;
-
let ncic_name_of_ident = function
| Ast.Ident (name, None) -> name
| _ -> assert false
uri, height, [], [],
(match bo,flavour with
| None,`Axiom ->
- let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+ let attrs = `Provided, flavour, pragma in
NCic.Constant ([],name,None,ty',attrs)
| Some _,`Axiom -> assert false
| None,_ ->
- let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+ let attrs = `Provided, 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, pragma in
+ let attrs = `Provided, 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, pragma in
+ let attrs = `Provided, flavour, pragma in
NCic.Constant ([],name,Some bo,ty',attrs)))
| NotationPt.Inductive (params,tyl) ->
let context,params =