aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--printing/printer.ml44
-rw-r--r--printing/printer.mli8
-rw-r--r--test-suite/output/Arguments_renaming.out2
-rw-r--r--test-suite/output/Existentials.out6
-rw-r--r--test-suite/output/Notations3.out8
-rw-r--r--test-suite/output/inference.out8
-rw-r--r--vernac/vernacentries.ml4
7 files changed, 45 insertions, 35 deletions
diff --git a/printing/printer.ml b/printing/printer.ml
index d720bc2f8..c38a73d7d 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -537,7 +537,7 @@ let pr_evgl_sign sigma evi =
let ids = List.rev_map NamedDecl.get_id l in
let warn =
if List.is_empty ids then mt () else
- (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)")
+ (str " (" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)")
in
let pc = pr_lconstr_env env sigma evi.evar_concl in
let candidates =
@@ -549,7 +549,7 @@ let pr_evgl_sign sigma evi =
mt ()
in
hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++
- candidates ++ spc () ++ warn)
+ candidates ++ warn)
(* Print an existential variable *)
@@ -558,15 +558,25 @@ let pr_evar sigma (evk, evi) =
hov 0 (pr_existential_key sigma evk ++ str " : " ++ pegl)
(* Print an enumerated list of existential variables *)
-let rec pr_evars_int_hd head sigma i = function
+let rec pr_evars_int_hd pr sigma i = function
| [] -> mt ()
| (evk,evi)::rest ->
- (hov 0 (head i ++ pr_evar sigma (evk,evi))) ++
- (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd head sigma (i+1) rest)
-
-let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ int i ++ str " =" ++ spc ()) sigma i (Evar.Map.bindings evs)
-
-let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs)
+ (hov 0 (pr i evk evi)) ++
+ (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd pr sigma (i+1) rest)
+
+let pr_evars_int sigma ~shelf ~givenup i evs =
+ let pr_status i =
+ if List.mem i shelf then str " (shelved)"
+ else if List.mem i givenup then str " (given up)"
+ else mt () in
+ pr_evars_int_hd
+ (fun i evk evi ->
+ str "Existential " ++ int i ++ str " =" ++
+ spc () ++ pr_evar sigma (evk,evi) ++ pr_status evk)
+ sigma i (Evar.Map.bindings evs)
+
+let pr_evars sigma evs =
+ pr_evars_int_hd (fun i evk evi -> pr_evar sigma (evk,evi)) sigma 1 (Evar.Map.bindings evs)
(* Display a list of evars given by their name, with a prefix *)
let pr_ne_evar_set hd tl sigma l =
@@ -684,7 +694,7 @@ let print_dependent_evars gl sigma seeds =
(* spiwack: [pr_first] is true when the first goal must be singled out
and printed in its entirety. *)
let default_pr_subgoals ?(pr_first=true)
- close_cmd sigma seeds shelf stack unfocused goals =
+ close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals =
(** Printing functions for the extra informations. *)
let rec print_stack a = function
| [] -> Pp.int a
@@ -746,7 +756,7 @@ let default_pr_subgoals ?(pr_first=true)
if Evar.Map.is_empty exl then
(str"No more subgoals." ++ print_dependent_evars None sigma seeds)
else
- let pei = pr_evars_int sigma 1 exl in
+ let pei = pr_evars_int sigma ~shelf ~givenup:[] 1 exl in
v 0 ((str "No more subgoals,"
++ str " but there are non-instantiated existential variables:"
++ cut () ++ (hov 0 pei)
@@ -773,7 +783,7 @@ let default_pr_subgoals ?(pr_first=true)
type printer_pr = {
- pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
+ 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;
}
@@ -807,16 +817,16 @@ let pr_open_subgoals ~proof =
begin match goals with
| [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
begin match bgoals,shelf,given_up with
- | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack [] goals
+ | [] , [] , [] -> pr_subgoals None sigma ~seeds ~shelf ~stack ~unfocused:[] ~goals
| [] , [] , _ ->
Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:");
fnl ()
- ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] given_up
+ ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:given_up
++ fnl () ++ str "You need to go back and solve them."
| [] , _ , _ ->
Feedback.msg_info (str "All the remaining goals are on the shelf.");
fnl ()
- ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] shelf
+ ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:shelf
| _ , _, _ ->
let end_cmd =
str "This subproof is complete, but there are some unfocused goals." ++
@@ -824,13 +834,13 @@ let pr_open_subgoals ~proof =
if Pp.ismt s then s else fnl () ++ s) ++
fnl ()
in
- pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] [] bgoals
+ pr_subgoals ~pr_first:false (Some end_cmd) bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals
end
| _ ->
let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in
let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in
- pr_subgoals ~pr_first:true None bsigma seeds shelf [] unfocused_if_needed bgoals_focused
+ pr_subgoals ~pr_first:true None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused
end
let pr_nth_open_subgoal ~proof n =
diff --git a/printing/printer.mli b/printing/printer.mli
index a3427920a..9b26d4c84 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -181,8 +181,7 @@ val pr_goal : goal sigma -> Pp.t
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 -> Evar.t list -> Goal.goal list -> int list
- -> goal list -> goal list -> Pp.t
+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
val pr_subgoal : int -> evar_map -> goal list -> Pp.t
val pr_concl : int -> evar_map -> goal -> Pp.t
@@ -190,7 +189,7 @@ val pr_concl : int -> evar_map -> goal -> 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
-val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> Pp.t
+val pr_evars_int : evar_map -> shelf:goal list -> givenup:goal list -> int -> evar_info Evar.Map.t -> Pp.t
val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t
val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map ->
Evar.Set.t -> Pp.t
@@ -223,7 +222,8 @@ 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 -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
+ 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;
}
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 4df21ae35..e73312c67 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -11,7 +11,7 @@ notation scopes add ': clear scopes' [arguments-assert,vernacular]
eq_refl
: ?y = ?y
where
-?y : [ |- nat]
+?y : [ |- nat]
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
For eq_refl: Arguments are renamed to B, y
diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out
index 9680d2bbf..18f5d89f6 100644
--- a/test-suite/output/Existentials.out
+++ b/test-suite/output/Existentials.out
@@ -1,4 +1,4 @@
-Existential 1 = ?Goal : [p : nat q := S p : nat n : nat m : nat |- ?y = m]
+Existential 1 = ?Goal : [p : nat q := S p : nat n : nat m : nat |- ?y = m]
Existential 2 =
-?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used)
-Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y]
+?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used) (shelved)
+Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y]
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index e6a6e0288..864b6151a 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -33,24 +33,24 @@ fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f
: (forall x : nat * (bool * unit), ?T) ->
forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))}
where
-?T : [x : nat * (bool * unit) |- Type]
+?T : [x : nat * (bool * unit) |- Type]
fun f : forall x : bool * (nat * unit), ?T =>
CURRYINV (x : nat) (y : bool), f
: (forall x : bool * (nat * unit), ?T) ->
forall (x : nat) (y : bool), ?T@{x:=(y, (x, tt))}
where
-?T : [x : bool * (nat * unit) |- Type]
+?T : [x : bool * (nat * unit) |- Type]
fun f : forall x : unit * nat * bool, ?T => CURRYLEFT (x : nat) (y : bool), f
: (forall x : unit * nat * bool, ?T) ->
forall (x : nat) (y : bool), ?T@{x:=(tt, x, y)}
where
-?T : [x : unit * nat * bool |- Type]
+?T : [x : unit * nat * bool |- Type]
fun f : forall x : unit * bool * nat, ?T =>
CURRYINVLEFT (x : nat) (y : bool), f
: (forall x : unit * bool * nat, ?T) ->
forall (x : nat) (y : bool), ?T@{x:=(tt, y, x)}
where
-?T : [x : unit * bool * nat |- Type]
+?T : [x : unit * bool * nat |- Type]
forall n : nat, {#n | 1 > n}
: Prop
forall x : nat, {|x | x > 0|}
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index d28ee4276..5e9eff048 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -9,10 +9,10 @@ fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
fun n : nat => let y : T n := A n in ?t ?x : T n
: forall n : nat, T n
where
-?t : [n : nat y := A n : T n |- ?T -> T n]
-?x : [n : nat y := A n : T n |- ?T]
+?t : [n : nat y := A n : T n |- ?T -> T n]
+?x : [n : nat y := A n : T n |- ?T]
fun n : nat => ?t ?x : T n
: forall n : nat, T n
where
-?t : [n : nat |- ?T -> T n]
-?x : [n : nat |- ?T]
+?t : [n : nat |- ?T -> T n]
+?x : [n : nat |- ?T]
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index fa457c895..bab5c5ae9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -63,8 +63,8 @@ let show_proof () =
let show_top_evars () =
(* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
let pfts = Proof_global.give_me_the_proof () in
- let gls,_,_,_,sigma = Proof.proof pfts in
- pr_evars_int sigma 1 (Evd.undefined_map sigma)
+ let gls,_,shelf,givenup,sigma = Proof.proof pfts in
+ pr_evars_int sigma ~shelf ~givenup 1 (Evd.undefined_map sigma)
let show_universes () =
let pfts = Proof_global.give_me_the_proof () in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 10:20:16 +0000