diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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) |