From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 26 Jan 2016 16:56:33 +0100
Subject: Imported Upstream version 8.5

---
 pretyping/typing.ml | 20 ++++++++++++++++----
 1 file changed, 16 insertions(+), 4 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index fb5927db..eb16628b 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -144,8 +144,13 @@ let e_judge_of_cast env evdref cj k tj =
   { uj_val = mkCast (cj.uj_val, k, expected_type);
     uj_type = expected_type }
 
-(* The typing machine without information, without universes but with
-   existential variables. *)
+let enrich_env env evdref =
+  let penv = Environ.pre_env env in
+  let penv' = Pre_env.({ penv with env_stratification =
+    { penv.env_stratification with env_universes = Evd.universes !evdref } }) in
+  Environ.env_of_pre_env penv'
+			  
+(* The typing machine with universes and existential variables. *)
 
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
@@ -264,6 +269,7 @@ and execute_recdef env evdref (names,lar,vdef) =
 and execute_array env evdref = Array.map (execute env evdref)
 
 let check env evdref c t =
+  let env = enrich_env env evdref in
   let j = execute env evdref c in
   if not (Evarconv.e_cumul env evdref j.uj_type t) then
     error_actual_type env j (nf_evar !evdref t)
@@ -271,12 +277,15 @@ let check env evdref c t =
 (* Type of a constr *)
 
 let unsafe_type_of env evd c =
-  let j = execute env (ref evd) c in
+  let evdref = ref evd in
+  let env = enrich_env env evdref in
+  let j = execute env evdref c in
     j.uj_type
 
 (* Sort of a type *)
 
 let sort_of env evdref c =
+  let env = enrich_env env evdref in
   let j = execute env evdref c in
   let a = e_type_judgment env evdref j in
   a.utj_type
@@ -285,6 +294,7 @@ let sort_of env evdref c =
 
 let type_of ?(refresh=false) env evd c =
   let evdref = ref evd in
+  let env = enrich_env env evdref in
   let j = execute env evdref c in
   (* side-effect on evdref *)
     if refresh then
@@ -292,6 +302,7 @@ let type_of ?(refresh=false) env evd c =
     else !evdref, j.uj_type
 
 let e_type_of ?(refresh=false) env evdref c =
+  let env = enrich_env env evdref in
   let j = execute env evdref c in
   (* side-effect on evdref *)
     if refresh then
@@ -301,6 +312,7 @@ let e_type_of ?(refresh=false) env evdref c =
     else j.uj_type
 
 let solve_evars env evdref c =
+  let env = enrich_env env evdref in
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
   nf_evar !evdref c
-- 
cgit v1.2.3