diff options
| author | Matthieu Sozeau | 2014-08-30 18:48:11 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-30 18:53:32 +0200 |
| commit | 437b91a3ffd7327975a129b95b24d3f66ad7f3e4 (patch) | |
| tree | 3e5b4098318c4bbad4024d072c5008825e78c1c9 /printing/printer.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 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 55a7d36a3c..ed872afc67 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -778,7 +778,7 @@ let print_mutual_inductive env mind mib = str (if mib.mind_finite then "Inductive " else "CoInductive ") ++ prlist_with_sep (fun () -> fnl () ++ str" with ") (print_one_inductive env mib) inds ++ - pr_universe_ctx mib.mind_universes) + pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) let get_fields = let rec prodec_rec l subst c = @@ -820,7 +820,7 @@ let print_record env mind mib = (fun (id,b,c) -> pr_id id ++ str (if b then " : " else " := ") ++ pr_lconstr_env envpar c) fields) ++ str" }" ++ - pr_universe_ctx mib.mind_universes) + pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes)) let pr_mutual_inductive_body env mind mib = if mib.mind_record <> None && not !Flags.raw_print then |