From fea52cee63b678dfda766a0a63435c134d28d77c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 5 Nov 2019 15:06:23 +0100
Subject: Fix #11048: uncaught destKO in inductive type

Reduction.whd_all does not commute with to_constr.
---
 vernac/comInductive.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'vernac/comInductive.ml')

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 36aa7a37a2..80fcb7bc45 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -12,7 +12,6 @@ open Pp
 open CErrors
 open Sorts
 open Util
-open Constr
 open Context
 open Environ
 open Names
@@ -164,9 +163,7 @@ let sign_level env evd sign =
       match d with
       | LocalDef _ -> lev, push_rel d env
       | LocalAssum _ ->
-        let s = destSort (Reduction.whd_all env
-                            (EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d)))))
-        in
+        let s = Retyping.get_sort_of env evd (EConstr.of_constr (RelDecl.get_type d)) in
         let u = univ_of_sort s in
           (Univ.sup u lev, push_rel d env))
     sign (Univ.Universe.sprop,env))
-- 
cgit v1.2.3