diff options
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 |