From 7d3c337a3b9f0906de22ccfde02203b8fafd330d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 4 Aug 2014 16:31:29 -0400
Subject: Fix an exponential behavior in guard checker for cofixpoints.

I had introduced it by mistake due to my OCaml dyslexia :)
Thanks to Enrico and Arnaud for saving my day!
---
 kernel/inductive.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index dfed980714..f3466c9200 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1107,9 +1107,10 @@ let check_one_cofix env nbfix def deftype =
                     then process_args_of_constr (lr, lrar)
                     else raise (CoFixGuardError
 		                 (env,RecCallInNonRecArgOfConstructor t))
-                  else
-                    check_rec_call env true n rar t;
-                    process_args_of_constr (lr, lrar)
+                  else begin
+                      check_rec_call env true n rar t;
+                      process_args_of_constr (lr, lrar)
+		    end
               | [],_ -> ()
               | _ -> anomaly_ill_typed ()
             in process_args_of_constr (realargs, lra)
-- 
cgit v1.2.3