diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 5e5d00362..fd7135b6a 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -40,7 +40,7 @@ type object_pr = { print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; - print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; @@ -246,13 +246,13 @@ let print_type_in_type ref = else [] let print_primitive_record recflag mipv = function - | Some (Some (_, ps,_)) -> + | PrimRecord _ -> let eta = match recflag with | CoFinite | Finite -> str" without eta conversion" | BiFinite -> str " with eta conversion" in [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] - | _ -> [] + | FakeRecord | NotRecord -> [] let print_primitive ref = match ref with |