aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/genprint.ml4
-rw-r--r--printing/genprint.mli4
-rw-r--r--printing/ppconstr.ml11
-rw-r--r--printing/ppconstr.mli4
-rw-r--r--printing/pputils.ml4
-rw-r--r--printing/pputils.mli4
-rw-r--r--printing/printer.ml8
-rw-r--r--printing/printer.mli12
-rw-r--r--printing/printmod.ml4
-rw-r--r--printing/printmod.mli4
-rw-r--r--printing/proof_diffs.ml8
-rw-r--r--printing/proof_diffs.mli6
12 files changed, 38 insertions, 35 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml
index a673cbd933..0157c066b6 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.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 *)
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 59e36baeb6..64ec8a57df 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -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 *)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 59972f8bdb..b285c0abcc 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.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 *)
@@ -77,8 +77,8 @@ let tag_var = tag Tag.variable
| LevelSome -> true
let prec_of_prim_token = function
- | Numeral (SPlus,_) -> lposint
- | Numeral (SMinus,_) -> lnegint
+ | Numeral (NumTok.SPlus,_) -> lposint
+ | Numeral (NumTok.SMinus,_) -> lnegint
| String _ -> latom
let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps =
@@ -222,8 +222,7 @@ let tag_var = tag Tag.variable
| t -> str " :" ++ pr_sep_com (fun()->brk(1,4)) (pr ltop) t
let pr_prim_token = function
- | Numeral (SPlus,n) -> str (NumTok.to_string n)
- | Numeral (SMinus,n) -> str ("-"^NumTok.to_string n)
+ | Numeral n -> NumTok.Signed.print n
| String s -> qs s
let pr_evar pr id l =
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 288fb251c4..2850e4bfa0 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -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 *)
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 5ec2f93cd8..896d38523a 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.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 *)
diff --git a/printing/pputils.mli b/printing/pputils.mli
index f260c4a373..479db15fff 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -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 *)
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)
diff --git a/printing/printer.mli b/printing/printer.mli
index 24d0a8cf6a..936426949c 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -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 *)
@@ -45,6 +45,10 @@ val enable_goal_names_printing : bool ref
intended to be printed in scope [some_scope_name]. It defaults to
[None].
+ [~impargs:some_list_of_binding_kind] indicates the implicit arguments
+ of the external quatification. Only used for printing types (not
+ terms), and at toplevel (only "l" versions). It defaults to [None].
+
[~lax:true] is for debugging purpose. It defaults to [~lax:false]. *)
@@ -66,7 +70,7 @@ val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -
val pr_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> EConstr.t -> Pp.t
val pr_etype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t
-val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t
+val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Pp.t
val pr_open_constr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t
val pr_open_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t
@@ -97,7 +101,7 @@ val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp
[~lax:true] is for debugging purpose. *)
-val pr_ltype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t
+val pr_ltype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> ?impargs:Glob_term.binding_kind list -> types -> Pp.t
val pr_type_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t
val pr_closed_glob_n_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> closed_glob_constr -> Pp.t
diff --git a/printing/printmod.ml b/printing/printmod.ml
index b84113bde2..eec2fe86ac 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.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 *)
diff --git a/printing/printmod.mli b/printing/printmod.mli
index 4c9245ee27..c7f056063b 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -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 *)
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index e4e1547b85..d73d1f2d1a 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.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 *)
@@ -242,9 +242,9 @@ let process_goal sigma g : EConstr.t reified_goal =
let hyps = List.map to_tuple hyps in
{ name; ty; hyps; env; sigma };;
-let pr_letype_env ?lax ?goal_concl_style env sigma t =
+let pr_letype_env ?lax ?goal_concl_style env sigma ?impargs t =
Ppconstr.pr_lconstr_expr env sigma
- (Constrextern.extern_type ?lax ?goal_concl_style env sigma t)
+ (Constrextern.extern_type ?lax ?goal_concl_style env sigma ?impargs t)
let pp_of_type env sigma ty =
pr_letype_env ~goal_concl_style:true env sigma ty
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index 477c0ce141..24b171770a 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -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 *)
@@ -57,7 +57,7 @@ val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t
(** Convert a string to a list of token strings using the lexer *)
val tokenize_string : string -> string list
-val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t
+val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Pp.t
val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
val pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> env -> evar_map -> constr -> Pp.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 16:03:11 +0000