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 ->
+ 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.Implicit `Vector -> NCic.Implicit `Vector
| CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
| CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)