From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 7 Apr 2008 16:17:16 +0000 (+0000)
Subject: uris relative to axioms are translated in the right way
X-Git-Tag: make_still_working~5422
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c10c2e70616edc42e155530e6bdd4a2e680f45f0;p=helm.git

uris relative to axioms are translated in the right way
---

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, _) ->