From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 pretyping/retyping.ml | 23 +++++++++--------------
 1 file changed, 9 insertions(+), 14 deletions(-)

(limited to 'pretyping/retyping.ml')

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3582b644..7e43c5e4 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -57,8 +57,8 @@ let get_type_from_constraints env sigma t =
   if isEvar sigma (fst (decompose_app_vect sigma t)) then
     match
       List.map_filter (fun (pbty,env,t1,t2) ->
-        if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t1) then Some t2
-        else if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t2) then Some t1
+        if is_fconv Reduction.CONV env sigma t t1 then Some t2
+        else if is_fconv Reduction.CONV env sigma t t2 then Some t1
         else None)
         (snd (Evd.extract_all_conv_pbs sigma))
     with
@@ -99,7 +99,7 @@ let retype ?(polyprop=true) sigma =
   let rec type_of env cstr =
     match EConstr.kind sigma cstr with
     | Meta n ->
-      (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus)
+      (try strip_outer_cast sigma (Evd.meta_ftype sigma n).Evd.rebus
        with Not_found -> retype_error (BadMeta n))
     | Rel n ->
 	let ty = RelDecl.get_type (lookup_rel n env) in
@@ -115,7 +115,7 @@ let retype ?(polyprop=true) sigma =
           try Inductiveops.find_rectype env sigma t
           with Not_found ->
           try
-            let t = EConstr.of_constr (get_type_from_constraints env sigma t) in
+            let t = get_type_from_constraints env sigma t in
             Inductiveops.find_rectype env sigma t
           with Not_found -> retype_error BadRecursiveType
         in
@@ -149,18 +149,13 @@ let retype ?(polyprop=true) sigma =
     | Cast (c,_, s) when isSort sigma s -> destSort sigma s
     | Sort s ->
       begin match ESorts.kind sigma s with
-      | Prop _ -> Sorts.type1
+      | Prop | Set -> Sorts.type1
       | Type u -> Type (Univ.super u)
       end
     | Prod (name,t,c2) ->
-        (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with
-	  | _, (Prop Null as s) -> s
-          | Prop _, (Prop Pos as s) -> s
-          | Type _, (Prop Pos as s) when is_impredicative_set env -> s
-          | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.type0_univ)
-	  | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2)
-	  | Prop Null, (Type _ as s) -> s
-	  | Type u1, Type u2 -> Type (Univ.sup u1 u2))
+      let dom = sort_of env t in
+      let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in
+      Typeops.sort_of_product env dom rang
     | App(f,args) when is_template_polymorphic env sigma f ->
       let t = type_of_global_reference_knowing_parameters env f args in
         sort_of_atomic_type env sigma t args
@@ -170,7 +165,7 @@ let retype ?(polyprop=true) sigma =
 
   and type_of_global_reference_knowing_parameters env c args =
     let argtyps =
-      Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in
+      Array.map (fun c -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma (type_of env c))) args in
     match EConstr.kind sigma c with
     | Ind (ind, u) ->
       let u = EInstance.kind sigma u in
-- 
cgit v1.2.3