Reports improved.

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 5bb6b93e29867c253037b142794a99338f1897e9..095b967a495975606fbc84ff1cedb2907ee93f39 100644 (file)
--- 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, _) -> 
@@ -262,6 +267,6 @@ let convert_obj_aux uri = function
 
 let convert_obj uri obj = 
   let o, fixpoints = convert_obj_aux uri obj in
-  let obj = NUri.nuri_of_ouri uri,0, [], [], o in
+  let obj = NUri.nuri_of_ouri uri,max_int, [], [], o in
   fixpoints @ [obj]
 ;;