From cdf961716bc825f362ea98b73be8e6a6201d52f0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 2 Mar 2020 02:06:08 -0500
Subject: [lemma] Remove double normalization of types

It should be safe now after previous refactoring in lemmas.
---
 vernac/vernacentries.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 30a1475e60..f935cea534 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -496,15 +496,10 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
     let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in
     let ids = List.map Context.Rel.Declaration.get_name ctx in
     check_name_freshness scope id;
-    (* XXX: The nf_evar is critical !! *)
-    evd, (id.CAst.v,
-          (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx),
-           (ids, imps @ imps'))))
+    evd, (id.CAst.v, (EConstr.it_mkProd_or_LetIn t' ctx, (ids, imps @ imps'))))
       evd thms in
   let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in
   let evd = Evd.minimize_universes evd in
-  (* XXX: This nf_evar is critical too!! We are normalizing twice if
-     you look at the previous lines... *)
   let thms = List.map (fun (name, (typ, (args, impargs))) ->
       { Lemmas.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in
   let () =
-- 
cgit v1.2.3