From 15f914ea52e7f3ec2bf00ec740d9a9935559b859 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Apr 2008 14:48:14 +0000 Subject: [PATCH] leftno should be increased of the expnamedsubst, but counting only the uris of vars without a body --- helm/software/components/ng_kernel/oCic2NCic.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index d66f45bd1..4aaeb414c 100644 --- 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 -- 2.39.2