From 0fff401b5c12a2d0684c8ff4980ebd9716f93905 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 13 Nov 2020 13:17:21 +0100
Subject: Extend hack to use postponed constraints in retyping to template poly

See 742ef62fe8050a6865d06bd644e30cbec0e7eb02

Fix #13366
Fix #9809
---
 pretyping/retyping.ml | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 4bd22e76cb..34bcd0982c 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -67,6 +67,14 @@ let get_type_from_constraints env sigma t =
     | _ -> raise Not_found
   else raise Not_found
 
+let sort_of_arity_with_constraints env sigma t =
+  try Reductionops.sort_of_arity env sigma t
+  with Reduction.NotArity ->
+  try
+    let t = get_type_from_constraints env sigma t in
+    Reductionops.sort_of_arity env sigma t
+  with Not_found | Reduction.NotArity -> retype_error NotAnArity
+
 let rec subst_type env sigma typ = function
   | [] -> typ
   | h::rest ->
@@ -187,9 +195,7 @@ let retype ?(polyprop=true) sigma =
       let mip = lookup_mind_specif env ind in
       let paramtyps = Array.map_to_list (fun arg () ->
           let t = type_of env arg in
-          let s = try Reductionops.sort_of_arity env sigma t
-            with Reduction.NotArity -> retype_error NotAnArity
-          in
+          let s = sort_of_arity_with_constraints env sigma t in
           Sorts.univ_of_sort (ESorts.kind sigma s))
           args
       in
-- 
cgit v1.2.3