diff options
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 20 |
1 files changed, 16 insertions, 4 deletions
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 |