From 10c81e90a836c8abea32bc6157976b9adf7775fa Mon Sep 17 00:00:00 2001 From: Julien Forest Date: Thu, 29 Jun 2017 17:27:04 +0200 Subject: closing bug #5618 introduce by PR 828 --- plugins/funind/indfun.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind/indfun.ml') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 35f092958..2c5dae1cd 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -593,7 +593,7 @@ and rebuild_nal aux bk bl' nal typ = | na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } -> if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na') then - let assum = CLocalAssum([na],bk',nal't) in + let assum = CLocalAssum([na],bk,nal't) in let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in rebuild_nal (assum::aux) @@ -602,7 +602,7 @@ and rebuild_nal aux bk bl' nal typ = nal (CAst.make @@ CProdN(new_rest,typ')) else - let assum = CLocalAssum([na'],bk',nal't) in + let assum = CLocalAssum([na'],bk,nal't) in let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in rebuild_nal (assum::aux) -- cgit v1.2.3