diff options
| author | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
| commit | c70412ec8b0bb34b7a5607c07d34607a147d834c (patch) | |
| tree | 0cc6cd76a8f70dfd2f5b55b0db96db4de2ff07a2 /printing/prettyp.ml | |
| parent | 720ee2730684cc289cef588482323d177e0bea59 (diff) | |
| parent | 191e253d1d1ebd6c76c63b3d83f4228e46196a6e (diff) | |
Merge PR #6914: Primitive integers
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 408bd5f60b..e0403a9f97 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -193,7 +193,7 @@ let opacity env = | ConstRef cst -> let cb = Environ.lookup_constant cst env in (match cb.const_body with - | Undef _ -> None + | Undef _ | Primitive _ -> None | OpaqueDef _ -> Some FullyOpaque | Def _ -> Some (TransparentMaybeOpacified @@ -558,7 +558,7 @@ let print_constant with_values sep sp udecl = let open Univ in let otab = Global.opaque_tables () in match cb.const_body with - | Undef _ | Def _ -> cb.const_universes + | Undef _ | Def _ | Primitive _ -> cb.const_universes | OpaqueDef o -> let body_uctxs = Opaqueproof.force_constraints otab o in match cb.const_universes with @@ -724,7 +724,10 @@ let print_full_pure_context env sigma = | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ - pr_lconstr_env env sigma (Mod_subst.force_constr c)) + pr_lconstr_env env sigma (Mod_subst.force_constr c) + | Primitive _ -> + str "Primitive " ++ + print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ) ++ str "." ++ fnl () ++ fnl () | "INDUCTIVE" -> let mind = Global.mind_of_delta_kn kn in |