From c10c2e70616edc42e155530e6bdd4a2e680f45f0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Apr 2008 16:17:16 +0000 Subject: [PATCH] uris relative to axioms are translated in the right way --- helm/software/components/ng_kernel/oCic2NCic.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index f20df7c80..095b967a4 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -203,7 +203,12 @@ let convert_term uri t = | (NCic.Appl l1)::l2 -> NCic.Appl (l1@l2), fixpoints | _ -> NCic.Appl l, fixpoints) | Cic.Const (curi, _) -> - NCic.Const (Ref.reference_of_ouri curi Ref.Def),[] + (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with + | Cic.Constant (_,Some _,_,_,_) -> + NCic.Const (Ref.reference_of_ouri curi Ref.Def),[] + | Cic.Constant (_,None,_,_,_) -> + NCic.Const (Ref.reference_of_ouri curi Ref.Decl),[] + | _ -> assert false) | Cic.MutInd (curi, tyno, _) -> NCic.Const (Ref.reference_of_ouri curi (Ref.Ind tyno)),[] | Cic.MutConstruct (curi, tyno, consno, _) -> -- 2.39.2