diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 33076a876b..9d896e9182 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -776,7 +776,7 @@ let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos let a' = infos.info in let new_info = { infos with - info = mkCase (ci, t, iv, a', l) + info = mkCase (ci, a, iv, a', l) ; is_main_branch = expr_info.is_main_branch ; is_final = expr_info.is_final } in |