leftno should be increased of the expnamedsubst, but counting only the uris of vars...

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index d66f45bd1f821c8da4c202bcfac1788b970c3ed1..4aaeb414c4d8330e70b6dc4cd3d224981b254f66 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -632,7 +632,14 @@ let convert_obj_aux uri = function
             ([], name, ty, cl)::itl, fix_ty @ fix_cl @ acc)
          itl ([],[])
      in
-     NCic.Inductive(ind, leftno + List.length vars, itl, (`Provided, `Regular)),
+     NCic.Inductive(ind, leftno + List.length 
+       (List.filter (fun v -> 
+          match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph v) with
+             Cic.Variable (_,Some _,_,_,_) -> false
+           | Cic.Variable (_,None,_,_,_) -> true
+           | _ -> assert false)
+          vars)
+       , itl, (`Provided, `Regular)),
      fix_itl
  | Cic.Variable _ 
  | Cic.CurrentProof _ -> assert false