Imported Upstream version 8.9.0upstream/8.9.0upstream

1 files changed, 56 insertions, 41 deletions

diff --git a/printing/printer.mli b/printing/printer.mli
index 41843680..518c5b93 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Globnames
 open Constr
 open Environ
 open Pattern
@@ -37,7 +36,7 @@ val pr_constr              : constr -> Pp.t
 [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
-val pr_constr_n_env        : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t
+val pr_constr_n_env        : env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t
 
 (** Same, but resilient to [Nametab] errors. Prints fully-qualified
     names when [shortest_qualid_of_global] has failed. Prints "??"
@@ -58,7 +57,7 @@ val pr_leconstr_env     : env -> evar_map -> EConstr.t -> Pp.t
 val pr_leconstr         : EConstr.t -> Pp.t
 [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
-val pr_econstr_n_env    : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t
+val pr_econstr_n_env    : env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t
 
 val pr_etype_env           : env -> evar_map -> EConstr.types -> Pp.t
 val pr_letype_env           : env -> evar_map -> EConstr.types -> Pp.t
@@ -88,7 +87,7 @@ val pr_type_env            : env -> evar_map -> types -> Pp.t
 val pr_type                : types -> Pp.t
 [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
-val pr_closed_glob_n_env   : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t
+val pr_closed_glob_n_env   : env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t
 val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> Pp.t
 val pr_closed_glob         : closed_glob_constr -> Pp.t
 [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
@@ -121,7 +120,7 @@ val pr_sort                : evar_map -> Sorts.t -> Pp.t
 
 val pr_polymorphic         : bool -> Pp.t
 val pr_cumulative          : bool -> bool -> Pp.t
-val pr_universe_instance   : evar_map -> Univ.UContext.t -> Pp.t
+val pr_universe_instance   : evar_map -> Univ.Instance.t -> Pp.t
 val pr_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
   Univ.UContext.t -> Pp.t
 val pr_universe_ctx_set    : evar_map -> Univ.ContextSet.t -> Pp.t
@@ -130,8 +129,8 @@ val pr_cumulativity_info   : evar_map -> Univ.CumulativityInfo.t -> Pp.t
 
 (** Printing global references using names as short as possible *)
 
-val pr_global_env          : Id.Set.t -> global_reference -> Pp.t
-val pr_global              : global_reference -> Pp.t
+val pr_global_env          : Id.Set.t -> GlobRef.t -> Pp.t
+val pr_global              : GlobRef.t -> Pp.t
 
 val pr_constant            : env -> Constant.t -> Pp.t
 val pr_existential_key     : evar_map -> Evar.t -> Pp.t
@@ -140,9 +139,9 @@ val pr_constructor         : env -> constructor -> Pp.t
 val pr_inductive           : env -> inductive -> Pp.t
 val pr_evaluable_reference : evaluable_global_reference -> Pp.t
 
-val pr_pconstant           : env -> pconstant -> Pp.t
-val pr_pinductive          : env -> pinductive -> Pp.t
-val pr_pconstructor        : env -> pconstructor -> Pp.t
+val pr_pconstant : env -> evar_map -> pconstant -> Pp.t
+val pr_pinductive : env -> evar_map -> pinductive -> Pp.t
+val pr_pconstructor : env -> evar_map -> pconstructor -> Pp.t
 
 
 (** Contexts *)
@@ -153,13 +152,13 @@ val get_compact_context : unit -> bool
 val pr_context_unlimited   : env -> evar_map -> Pp.t
 val pr_ne_context_of       : Pp.t -> env -> evar_map -> Pp.t
 
-val pr_named_decl          : env -> evar_map -> Context.Named.Declaration.t -> Pp.t
-val pr_compacted_decl      : env -> evar_map -> Context.Compacted.Declaration.t -> Pp.t
-val pr_rel_decl            : env -> evar_map -> Context.Rel.Declaration.t -> Pp.t
+val pr_named_decl          : env -> evar_map -> Constr.named_declaration -> Pp.t
+val pr_compacted_decl      : env -> evar_map -> Constr.compacted_declaration -> Pp.t
+val pr_rel_decl            : env -> evar_map -> Constr.rel_declaration -> Pp.t
 
-val pr_named_context       : env -> evar_map -> Context.Named.t -> Pp.t
+val pr_named_context       : env -> evar_map -> Constr.named_context -> Pp.t
 val pr_named_context_of    : env -> evar_map -> Pp.t
-val pr_rel_context         : env -> evar_map -> Context.Rel.t -> Pp.t
+val pr_rel_context         : env -> evar_map -> Constr.rel_context -> Pp.t
 val pr_rel_context_of      : env -> evar_map -> Pp.t
 val pr_context_of          : env -> evar_map -> Pp.t
 
@@ -172,22 +171,46 @@ val pr_transparent_state   : transparent_state -> Pp.t
 
 (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *)
 
-val pr_goal                : goal sigma -> Pp.t
-
-(** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals]
-   prints the goals of the list [goals] followed by the goals in
-   [unfocused], in a short way (typically only the conclusion) except
-   for the first goal if [pr_first] is true. This function can be
-   replaced by another one by calling [set_printer_pr] (see below),
-   typically by plugin writers. The default printer prints only the
-   focused goals unless the conrresponding option
-   [enable_unfocused_goal_printing] is set. [seeds] is for printing
-   dependent evars (mainly for emacs proof tree mode). *)
-val pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t
+(** [pr_goal ~diffs ~og_s g_s] prints the goal specified by [g_s].  If [diffs] is true,
+    highlight the differences between the old goal, [og_s], and [g_s].  [g_s] and [og_s] are
+    records containing the goal and sigma for, respectively, the new and old proof steps,
+    e.g. [{ it = g ; sigma = sigma }].
+*)
+val pr_goal                : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma -> Pp.t
+
+(** [pr_subgoals ~pr_first ~diffs ~os_map close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals]
+   prints the goals in [goals] followed by the goals in [unfocused] in a compact form
+   (typically only the conclusion).  If [pr_first] is true, print the first goal in full.
+   [close_cmd] is printed afterwards verbatim.
+
+   If [diffs] is true, then highlight diffs relative to [os_map] in the output for first goal.
+   [os_map] contains sigma for the old proof step and the goal map created by
+   [Proof_diffs.make_goal_map].
+
+   This function prints only the focused goals unless the corresponding option [enable_unfocused_goal_printing] is set.
+   [seeds] is for printing dependent evars (mainly for emacs proof tree mode).  [shelf] is from
+   Proof.proof and is used to identify shelved goals in a message if there are no more subgoals but
+   there are non-instantiated existential variables.  [stack] is used to print summary info on unfocused
+   goals.
+*)
+val pr_subgoals            : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Evar.t Evar.Map.t) -> Pp.t option -> evar_map
+                             -> seeds:goal list -> shelf:goal list -> stack:int list
+                             -> unfocused: goal list -> goals:goal list -> Pp.t
 
 val pr_subgoal             : int -> evar_map -> goal list -> Pp.t
-val pr_concl               : int -> evar_map -> goal -> Pp.t
 
+(** [pr_concl n ~diffs ~og_s sigma g] prints the conclusion of the goal [g] using [sigma].  The output
+    is labelled "subgoal [n]".  If [diffs] is true, highlight the differences between the old conclusion,
+    [og_s], and [g]+[sigma].  [og_s] is a record containing the old goal and sigma, e.g. [{ it = g ; sigma = sigma }].
+*)
+val pr_concl               : int -> ?diffs:bool -> ?og_s:(goal sigma) -> evar_map -> goal -> Pp.t
+
+(** [pr_open_subgoals_diff ~quiet ~diffs ~oproof proof] shows the context for [proof] as used by, for example, coqtop.
+    The first active goal is printed with all its antecedents and the conclusion.  The other active goals only show their
+     conclusions.  If [diffs] is true, highlight the differences between the old proof, [oproof], and [proof].  [quiet]
+     disables printing messages as Feedback.
+*)
+val pr_open_subgoals_diff  : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Proof.t -> Pp.t
 val pr_open_subgoals       : proof:Proof.t -> Pp.t
 val pr_nth_open_subgoal    : proof:Proof.t -> int -> Pp.t
 val pr_evar                : evar_map -> (Evar.t * evar_info) -> Pp.t
@@ -197,11 +220,14 @@ val pr_ne_evar_set         : Pp.t -> Pp.t -> evar_map ->
   Evar.Set.t -> Pp.t
 
 val pr_prim_rule           : prim_rule -> Pp.t
+[@@ocaml.deprecated "[pr_prim_rule] is scheduled to be removed along with the legacy proof engine"]
+
+val print_and_diff : Proof.t option -> Proof.t option -> unit
 
 (** Backwards compatibility *)
 
 val prterm                 : constr -> Pp.t (** = pr_lconstr *)
-
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 (** Declarations for the "Print Assumption" command *)
 type axiom =
@@ -211,7 +237,7 @@ type axiom =
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
-  | Axiom of axiom * (Label.t * Context.Rel.t * types) list
+  | Axiom of axiom * (Label.t * Constr.rel_context * types) list
   | Opaque of Constant.t     (* An opaque constant. *)
   | Transparent of Constant.t
 
@@ -223,14 +249,3 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t
 
 val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
 
-type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t;
-
- pr_subgoal             : int -> evar_map -> goal list -> Pp.t;
- pr_goal                : goal sigma -> Pp.t;
-}
-
-val set_printer_pr : printer_pr -> unit
-
-val default_printer_pr : printer_pr
-