From 50c948480647af3c5aaea5f80fa9f3341471f2b0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 13 Feb 2018 12:19:47 +0100
Subject: Fixing an anomaly in the presence of "let-in" in the type of a
 record.

Was raised by Jason on Gitter.
---
 vernac/record.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/record.ml b/vernac/record.ml
index d9af5378f4..95bcaf6dc3 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -121,7 +121,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
          match t with
          | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in
        let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in
-       let sred = Reductionops.whd_all env sigma s in
+       let sred = Reductionops.whd_allnolet env sigma s in
          (match EConstr.kind sigma sred with
 	 | Sort s' ->
             let s' = EConstr.ESorts.kind sigma s' in
-- 
cgit v1.2.3