diff options
| author | coqbot-app[bot] | 2020-12-02 11:00:04 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-02 11:00:04 +0000 |
| commit | ff8155bf6586040b92d916a72017ac1bdc138501 (patch) | |
| tree | 69744806c326313960ecb53c53d56ae7bf299928 | |
| parent | b3b4d641dafe58ad04932c5bb5cc2f4f3f54d91f (diff) | |
| parent | 64de97e5f16d3c52f73fb126ca64c85382c2a3d4 (diff) | |
Merge PR #13543: Fix a bug in funind.
Reviewed-by: Matafou
| -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 |