added leftno to references f inductive types and constructors, more unifor names...

[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 096834d40fbddd87998d31e94656b45947de40f7..aa546d773ca7821f43aada14e2562831ce9e66fa 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -646,29 +646,34 @@ let convert_term uri t =
                NCic.Const (reference_of_ouri curi Ref.Decl)
         | _ -> assert false)
     | Cic.MutInd (curi, tyno, ens) -> 
-       let is_inductive =
+       let is_inductive, lno =
         match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
-           Cic.InductiveDefinition ([],_,_,_) -> true
-         | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+           Cic.InductiveDefinition ([],_,lno,_) -> true, lno
+         | Cic.InductiveDefinition ((_,b,_,_)::_,_,lno,_) -> b, lno
          | _ -> assert false
        in
         aux_ens k curi octx ctx n_fix uri ens
-         (NCic.Const (reference_of_ouri curi (Ref.Ind (is_inductive,tyno))))
+         (NCic.Const (reference_of_ouri curi (Ref.Ind (is_inductive,tyno,lno))))
     | Cic.MutConstruct (curi, tyno, consno, ens) -> 
+       let lno =
+        match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+           Cic.InductiveDefinition (_,_,lno,_) -> lno
+         | _ -> assert false
+       in
        aux_ens k curi octx ctx n_fix uri ens
-        (NCic.Const (reference_of_ouri curi (Ref.Con (tyno,consno))))
+        (NCic.Const (reference_of_ouri curi (Ref.Con (tyno,consno,lno))))
     | Cic.Var (curi, ens) ->
        (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
            Cic.Variable (_,Some bo,_,_,_) ->
             aux k octx ctx n_fix uri (CicSubstitution.subst_vars ens bo)
          | _ -> assert false)
     | Cic.MutCase (curi, tyno, outty, t, branches) ->
-        let is_inductive =
+        let is_inductive,lno =
          match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
-            Cic.InductiveDefinition ([],_,_,_) -> true
-          | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+            Cic.InductiveDefinition ([],_,lno,_) -> true, lno
+          | Cic.InductiveDefinition ((_,b,_,_)::_,_,lno,_) -> b, lno
           | _ -> assert false in
-        let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno)) in
+        let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno,lno)) in
         let outty, fixpoints_outty = aux k octx ctx n_fix uri outty in
         let t, fixpoints_t = aux k octx ctx n_fix uri t in
         let branches, fixpoints =