diff options
| author | Emilio Jesus Gallego Arias | 2020-03-02 02:06:08 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-19 17:18:54 -0400 |
| commit | cdf961716bc825f362ea98b73be8e6a6201d52f0 (patch) | |
| tree | 44068cb291a61ad1dbda50c3d3906c5e1172cba3 | |
| parent | eb452f9da5a52df0d74f7a433cfe98e31ab4ab15 (diff) | |
[lemma] Remove double normalization of types
It should be safe now after previous refactoring in lemmas.
| -rw-r--r-- | vernac/vernacentries.ml | 7 |
1 files changed, 1 insertions, 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 () = |