diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-30 18:48:11 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-30 18:53:32 +0200 |
| commit | 437b91a3ffd7327975a129b95b24d3f66ad7f3e4 (patch) | |
| tree | 3e5b4098318c4bbad4024d072c5008825e78c1c9 /kernel/indtypes.ml | |
| parent | dac4d8952c5fc234f5b6245e39a73c2ca07555ee (diff) | |
Simplify even further the declaration of primitive projections,
now done entirely using declare_mind, which declares the associated
constants for primitive records. This avoids a hack related to
elimination schemes and ensures that the forward references to constants
in the mutual inductive entry are properly declared just after the
inductive. This also clarifies (and simplifies) the code of term_typing
for constants which does not have to deal with building
or checking projections anymore.
Also fix printing of universes showing the de Bruijn encoding in a few places.
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 7ae787d22..759d71206 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -782,7 +782,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re | Some true when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 -> (** The elimination criterion ensures that all projections can be defined. *) let rctx, _ = decompose_prod_assum pkt.mind_nf_lc.(0) in - let u = if p then Univ.UContext.instance ctx else Univ.Instance.empty in + let u = + if p then + subst_univs_level_instance subst (Univ.UContext.instance ctx) + else Univ.Instance.empty + in (try let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in let kns, projs = |