diff options
| author | Maxime Dénès | 2017-06-30 13:38:58 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-30 13:38:58 +0200 |
| commit | 654a7b390f4062d9962e42d83537aa520fe82f2b (patch) | |
| tree | e178c69677a6c8d769011f326033359c2b399255 /plugins | |
| parent | 6d7c392b73eaa021083ab03c9042d271fb4c28c0 (diff) | |
| parent | 10c81e90a836c8abea32bc6157976b9adf7775fa (diff) | |
Merge PR#843: closing bug #5618 introduce by PR 828
Diffstat (limited to 'plugins')
| -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 35f0929587..2c5dae1cde 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) |