diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-31 23:20:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-01 02:34:24 +0200 |
| commit | 3df2431a80f9817ce051334cb9c3b1f465bffb60 (patch) | |
| tree | db9ec5c21eeae52bb9bc4b391e261496835f03bc /pretyping/pretyping.ml | |
| parent | ce029533a1f0fc6ac9e28d162350a64446522246 (diff) | |
Actually exporting delayed universes in the EConstr implementation.
For now we only normalize sorts, and we leave instances for the next
commit.
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 846d8055a..c673851c8 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1071,7 +1071,11 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | GHole (loc, knd, naming, None) -> let rec is_Type c = match EConstr.kind !evdref c with - | Sort (Type _) -> true + | Sort s -> + begin match ESorts.kind !evdref s with + | Type _ -> true + | Prop _ -> false + end | Cast (c, _, _) -> is_Type c | _ -> false in @@ -1081,7 +1085,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function let sigma = !evdref in let t = Retyping.get_type_of env.ExtraEnv.env sigma v in match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with - | Sort s -> s + | Sort s -> ESorts.kind sigma s | Evar ev when is_Type (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type") |