diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-12 14:49:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 15:14:45 +0200 |
| commit | 71563ebb86a83bc7cdfc17f58493f59428d764b0 (patch) | |
| tree | 247d33d8021ede65e34ac6d2de3d4224f0c80e90 /printing/prettyp.ml | |
| parent | 1014de55656c2698500089d940a12f7e4b26a0de (diff) | |
Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index d1e51c9f3..a0c88a7af 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -798,9 +798,11 @@ let print_opaque_name qid = | IndRef (sp,_) -> print_inductive sp | ConstructRef cstr as gr -> - let open EConstr in - let ty = Universes.unsafe_type_of_global gr in + let ty, ctx = Global.type_of_global_in_context env gr in + let inst = Univ.AUContext.instance ctx in + let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in + let open EConstr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl |