diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | printing/prettyp.ml | 4 | ||||
| -rw-r--r-- | printing/printmod.ml | 6 |
3 files changed, 6 insertions, 6 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 418d4a0b8f..e88284fb1c 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1223,7 +1223,7 @@ open Decl_kinds let return = tag_vernac v in match v with | VernacExpr v' -> pr_vernac_expr v' ++ sep_end v' - | VernacTime (_,v) -> + | VernacTime (_,(_,v)) -> return (keyword "Time" ++ spc() ++ pr_vernac_control v) | VernacRedirect (s, (_,v)) -> return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 647111bbe1..2b7886d115 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -235,8 +235,8 @@ let print_type_in_type ref = let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> let eta = match recflag with - | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion" - | Decl_kinds.BiFinite -> str " with eta conversion" + | CoFinite | Finite -> str" without eta conversion" + | BiFinite -> str " with eta conversion" in [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] | _ -> [] diff --git a/printing/printmod.ml b/printing/printmod.ml index 05292b06ba..fb9d45a793 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -125,7 +125,7 @@ let print_mutual_inductive env mind mib udecl = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) in let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | Finite -> "Inductive" | BiFinite -> "Variant" @@ -184,7 +184,7 @@ let print_record env mind mib udecl = (Array.to_list (Univ.Instance.to_array u)) udecl in let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | BiFinite -> "Record" | Finite -> "Inductive" @@ -346,7 +346,7 @@ let print_body is_impl env mp (l,body) = pr_mutual_inductive_body env (MutInd.make2 mp l) mib None with e when CErrors.noncritical e -> let keyword = - let open Decl_kinds in + let open Declarations in match mib.mind_finite with | Finite -> def "Inductive" | BiFinite -> def "Variant" |