From 86d08ece4c63e2a42f72ddd3afc51ce04cd1932a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 28 Jun 2018 18:36:20 +0200
Subject: Fix an algorithmic issue in the vernac guardedness checker.

Calling the O(n) EConstr.to_constr function at every node is a very bad
idea (tm).
---
 pretyping/inductiveops.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index ec0ff73062..1ecd4773ae 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -750,8 +750,11 @@ let type_of_projection_knowing_arg env sigma p c ty =
    syntactic conditions *)
 
 let control_only_guard env sigma c =
+  let c = Evarutil.nf_evar sigma c in
   let check_fix_cofix e c =
-    match kind (EConstr.to_constr sigma c) with
+    (** [c] has already been normalized upfront *)
+    let c = EConstr.Unsafe.to_constr c in
+    match kind c with
     | CoFix (_,(_,_,_) as cofix) ->
       Inductive.check_cofix e cofix
     | Fix (_,(_,_,_) as fix) ->
-- 
cgit v1.2.3