diff options
| author | Pierre-Marie Pédrot | 2019-03-11 12:16:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-01 22:29:57 +0100 |
| commit | 64de97e5f16d3c52f73fb126ca64c85382c2a3d4 (patch) | |
| tree | 7b7342ed21790a0bacce8b97c79b7fc41a4db886 /plugins/funind | |
| parent | b39b55934269f288b03b19e05bad3dafaa447a55 (diff) | |
Fix a bug in funind.
It was generating a completely nonsense case branch, but for some reason
the proof still went trough.
Diffstat (limited to 'plugins/funind')
| -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 |