diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-13 00:25:21 +0530 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-13 00:29:09 +0530 |
| commit | c60f40ccecf526b5c7ce5adfe5908fdac3f66771 (patch) | |
| tree | cb0eb77577f7de305043d081dbf8e7ecacc02149 /printing | |
| parent | d797153f3e44279dd61804c3d2e75ec7892f38bf (diff) | |
Fix issue in printing due to de Bruijn bug when constructing compatibility
constr for primitive records (not used anywhere else than printing).
Problem reported by P. LeFanu Lumsdaine on HoTT/HoTT.
Also add some minor fixes in detyping and pretty printing related to universes.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 3cade3b7b..223377c27 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -472,7 +472,9 @@ let print_constant with_values sep sp = let val_0 = Global.body_of_constant_body cb in let typ = Declareops.type_of_constant cb in let typ = ungeneralized_type_of_constant_type typ in - let univs = Univ.instantiate_univ_context (Global.universes_of_constant_body cb) in + let univs = Univ.instantiate_univ_context + (Global.universes_of_constant_body cb) + in hov 0 (pr_polymorphic cb.const_polymorphic ++ match val_0 with | None -> @@ -720,8 +722,8 @@ let print_opaque_name qid = error "Not a defined constant." | IndRef (sp,_) -> print_inductive sp - | ConstructRef cstr -> - let ty = Inductiveops.type_of_constructor env (cstr,Univ.Instance.empty) in + | ConstructRef cstr as gr -> + let ty = Universes.unsafe_type_of_global gr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> let (_,c,ty) = lookup_named id env in |