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/typing.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/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index dec22ecd0..d9d64e7eb 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -46,7 +46,7 @@ let inductive_type_knowing_parameters env sigma (ind,u) jl = let e_type_judgment env evdref j = match EConstr.kind !evdref (whd_all env !evdref j.uj_type) with - | Sort s -> {utj_val = j.uj_val; utj_type = s } + | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind !evdref s } | Evar ev -> let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in evdref := evd; { utj_val = j.uj_val; utj_type = s } @@ -102,6 +102,7 @@ let e_is_correct_arity env evdref c pj ind specif params = if not (Evarconv.e_cumul env evdref a1 a1') then error (); srec (push_rel (LocalAssum (na1,a1)) env) t ar' | Sort s, [] -> + let s = ESorts.kind !evdref s in if not (Sorts.List.mem (Sorts.family s) allowed_sorts) then error () | Evar (ev,_), [] -> @@ -161,7 +162,7 @@ let check_type_fixpoint loc env evdref lna lar vdefj = (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let pj = Retyping.get_judgment_of env sigma p in - let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in + let ksort = family_of_sort (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in let specif = Global.lookup_inductive (fst ind) in let sorts = elim_sorts specif in if not (List.exists ((==) ksort) sorts) then @@ -288,11 +289,13 @@ let rec execute env evdref cstr = check_cofix env !evdref cofix; make_judge (mkCoFix cofix) tys.(i) - | Sort (Prop c) -> - judge_of_prop_contents c - - | Sort (Type u) -> + | Sort s -> + begin match ESorts.kind !evdref s with + | Prop c -> + judge_of_prop_contents c + | Type u -> judge_of_type u + end | Proj (p, c) -> let cj = execute env evdref c in |