From bef1dc9b45c34a9cf992ec96ea719ca6699960d3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 14:47:56 +0000 Subject: [PATCH] fix_outty partially fixed: missing lifts in args and ens --- helm/software/components/ng_kernel/oCic2NCic.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index d67089146..54e12be14 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -93,7 +93,8 @@ prerr_endline ("LEFTNO: " ^ string_of_int leftno ^ " " ^ CicPp.ppterm arity);*) match n, CicReduction.whd context outsort with 0, Cic.Prod _ -> raise Nothing_to_do | 0, _ -> - let ty = Cic.MutInd (curi,tyno,ens) in + let irl = List.rev irl in + let ty = CicSubstitution.lift rightno (Cic.MutInd (curi,tyno,ens)) in let ty = if args = [] && irl = [] then ty else -- 2.39.2