diff options
| author |  Julien Forest <forest@ensiie.fr> | 2017-06-29 17:27:04 +0200 |
|---|---|---|
| committer | Julien Forest <forest@ensiie.fr> | 2017-06-29 17:27:04 +0200 |
| commit | 10c81e90a836c8abea32bc6157976b9adf7775fa (patch) | |
| tree | a7c4f13cacb5ea4438ba3e062f45c8fd2f15b270 /plugins/funind | |
| parent | 181cb78d09ba55c7a6d62b333b26595a4fbb360a (diff) | |
closing bug #5618 introduce by PR 828
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) |