aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/printer.ml')
-rw-r--r--printing/printer.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/printing/printer.ml b/printing/printer.ml
index b376616b61..32dc4bb0f0 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -106,8 +106,8 @@ let pr_letype_env = Proof_diffs.pr_letype_env
let pr_type_env ?lax ?goal_concl_style env sigma c =
pr_etype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c)
-let pr_ltype_env ?lax ?goal_concl_style env sigma c =
- pr_letype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c)
+let pr_ltype_env ?lax ?goal_concl_style env sigma ?impargs c =
+ pr_letype_env ?lax ?goal_concl_style env sigma ?impargs (EConstr.of_constr c)
let pr_ljudge_env env sigma j =
(pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)