From a6b2029042ae2e5f51fcae6d922fc8437ae1ff13 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 19 Apr 2020 12:58:05 +0200
Subject: Warn when a (co)fixpoint is not truly recursive.

---
 plugins/funind/gen_principle.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 55e659d487..600e11afc4 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -159,7 +159,7 @@ let recompute_binder_list fixpoint_exprl =
       fixpoint_exprl
   in
   let (_, _, _, typel), _, ctx, _ =
-    ComFixpoint.interp_fixpoint ~cofix:false fixl
+    ComFixpoint.interp_fixpoint ~check_recursivity:false ~cofix:false fixl
   in
   let constr_expr_typel =
     with_full_print
-- 
cgit v1.2.3