From 64de97e5f16d3c52f73fb126ca64c85382c2a3d4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 Mar 2019 12:16:45 +0100
Subject: Fix a bug in funind.

It was generating a completely nonsense case branch, but for some reason
the proof still went trough.
---
 plugins/funind/recdef.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

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
-- 
cgit v1.2.3