From 2794b3c91bbbef115303b40f2e494ad97467dc9e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 5 Apr 2017 14:05:42 +0200
Subject: Removing a normalization hotspot from EConstr.

It was not necessary to normalize a term just to check whether it was a
global reference. The hotspot appeared in mathcomp.
---
 pretyping/evarconv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 9c9350ab10..44b771283b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -154,7 +154,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
 	lookup_canonical_conversion
 	  (proji, Sort_cs (family_of_sort s)),[]
       | _ ->
-	let c2 = global_of_constr (EConstr.to_constr sigma t2) in
+	let (c2, _) = Termops.global_of_constr sigma t2 in
 	  lookup_canonical_conversion (proji, Const_cs c2),sk2
     with Not_found ->
       let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in 
-- 
cgit v1.2.3