From 1c4968498b6f108cd9c4074c177845a4067cd9d6 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 8 Jun 2010 16:15:14 +0000 Subject: [PATCH] Fixed a bug in the undebruijnate function which caused the refiner to produce a wrong object when refining mutually recursive functions (the references to recursive calls would contain the wrong index to the recursive argument). --- helm/software/components/ng_refiner/nCicRefiner.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 7833b9c4a..ec4747781 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -993,13 +993,15 @@ let relocalise old_localise dt t add = ;; let undebruijnate inductive ref t rev_fl = + let len = List.length rev_fl in NCicSubstitution.psubst (fun x -> x) - (List.rev (HExtlib.list_mapi + (HExtlib.list_mapi (fun (_,_,rno,_,_,_) i -> + let i = len - i - 1 in NCic.Const (if inductive then NReference.mk_fix i rno ref else NReference.mk_cofix i ref)) - rev_fl)) + rev_fl) t ;; -- 2.39.2