aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/printer.ml47
-rw-r--r--parsing/printer.mli4
-rw-r--r--proofs/proof.ml3
-rw-r--r--proofs/proof.mli3
-rw-r--r--proofs/proofview.ml6
-rw-r--r--proofs/proofview.mli3
6 files changed, 55 insertions, 11 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 8727f10228..1c357076c9 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -29,6 +29,8 @@ open Store.Field
let emacs_str s =
if !Flags.print_emacs then s else ""
+let delayed_emacs_cmd s =
+ if !Flags.print_emacs then s () else str ""
(**********************************************************************)
(** Terms *)
@@ -323,8 +325,28 @@ let default_pr_subgoal n sigma =
in
prrec n
+let emacs_print_dependent_evars sigma seeds =
+ let evars () =
+ let evars = Evarutil.evars_of_evars_in_types_of_list sigma seeds in
+ let evars =
+ Intmap.fold begin fun e i s ->
+ let e' = str (string_of_existential e) in
+ match i with
+ | None -> s ++ e' ++ str " open,"
+ | Some i ->
+ s ++ e' ++ str " using " ++
+ Intset.fold begin fun d s ->
+ str (string_of_existential d) ++ str " " ++ s
+ end i (str "")
+ end evars (str "")
+ in
+ str "(dependent evars: " ++ evars ++ str ")" ++ fnl ()
+ in
+ delayed_emacs_cmd evars
+
(* Print open subgoals. Checks for uninstantiated existential variables *)
-let default_pr_subgoals close_cmd sigma = function
+(* spiwack: [seeds] is for printing dependent evars in emacs mode. *)
+let default_pr_subgoals close_cmd sigma seeds = function
| [] ->
begin
match close_cmd with
@@ -342,7 +364,10 @@ let default_pr_subgoals close_cmd sigma = function
end
| [g] ->
let pg = default_pr_goal { it = g ; sigma = sigma } in
- v 0 (str ("1 "^"subgoal") ++ pr_goal_tag g ++ cut () ++ pg)
+ v 0 (
+ emacs_print_dependent_evars sigma seeds ++
+ str ("1 "^"subgoal") ++ pr_goal_tag g ++ cut () ++ pg
+ )
| g1::rest ->
let rec pr_rec n = function
| [] -> (mt ())
@@ -353,16 +378,19 @@ let default_pr_subgoals close_cmd sigma = function
in
let pg1 = default_pr_goal { it = g1 ; sigma = sigma } in
let prest = pr_rec 2 rest in
- v 0 (int(List.length rest+1) ++ str" subgoals" ++
- str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
- ++ pg1 ++ prest ++ fnl ())
+ v 0 (
+ emacs_print_dependent_evars sigma seeds ++
+ int(List.length rest+1) ++ str" subgoals" ++
+ str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
+ ++ pg1 ++ prest ++ fnl ()
+ )
(**********************************************************************)
(* Abstraction layer *)
type printer_pr = {
- pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds;
+ pr_subgoals : string option -> evar_map -> evar list -> goal list -> std_ppcmds;
pr_subgoal : int -> evar_map -> goal list -> std_ppcmds;
pr_goal : goal sigma -> std_ppcmds;
}
@@ -387,11 +415,12 @@ let pr_goal x = !printer_pr.pr_goal x
let pr_open_subgoals () =
let p = Proof_global.give_me_the_proof () in
let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in
+ let seeds = Proof.V82.top_evars p in
begin match goals with
| [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
begin match bgoals with
- | [] -> pr_subgoals None sigma goals
- | _ -> pr_subgoals None bsigma bgoals ++ fnl () ++ fnl () ++
+ | [] -> pr_subgoals None sigma seeds goals
+ | _ -> pr_subgoals None bsigma seeds bgoals ++ fnl () ++ fnl () ++
str"This subproof is complete, but there are still unfocused goals:"
(* spiwack: to stay compatible with the proof general and coqide,
I use print the message after the goal. It would be better to have
@@ -401,7 +430,7 @@ let pr_open_subgoals () =
instead. But it doesn't quite work.
*)
end
- | _ -> pr_subgoals None sigma goals
+ | _ -> pr_subgoals None sigma seeds goals
end
let pr_nth_open_subgoal n =
diff --git a/parsing/printer.mli b/parsing/printer.mli
index ff6d818072..2d437c2013 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -104,7 +104,7 @@ val pr_transparent_state : transparent_state -> std_ppcmds
(** Proofs *)
val pr_goal : goal sigma -> std_ppcmds
-val pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds
+val pr_subgoals : string option -> evar_map -> evar list -> goal list -> std_ppcmds
val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds
val pr_concl : int -> evar_map -> goal -> std_ppcmds
@@ -141,7 +141,7 @@ val pr_assumptionset :
val pr_goal_by_id : string -> std_ppcmds
type printer_pr = {
- pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds;
+ pr_subgoals : string option -> evar_map -> evar list -> goal list -> std_ppcmds;
pr_subgoal : int -> evar_map -> goal list -> std_ppcmds;
pr_goal : goal sigma -> std_ppcmds;
};;
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 8283657983..2aa31cd253 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -435,6 +435,9 @@ module V82 = struct
in
{ Evd.it=List.hd gls ; sigma=sigma }
+ let top_evars p =
+ Proofview.V82.top_evars p.state.proofview
+
let instantiate_evar n com pr =
let starting_point = save_state pr in
let sp = pr.state.proofview in
diff --git a/proofs/proof.mli b/proofs/proof.mli
index b4c84cbf60..d80ac79af2 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -171,6 +171,9 @@ module V82 : sig
val depth : proof -> int
val top_goal : proof -> Goal.goal Evd.sigma
+
+ (* returns the existential variable used to start the proof *)
+ val top_evars : proof -> Evd.evar list
(* Implements the Existential command *)
val instantiate_evar : int -> Topconstr.constr_expr -> proof -> unit
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index b76c802dfd..0d50d521f3 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -484,6 +484,12 @@ module V82 = struct
let goals = List.map (fun (t,_) -> Goal.V82.build (fst (Term.destEvar t))) initial in
{ Evd.it = goals ; sigma=solution }
+ let top_evars { initial=initial } =
+ let evars_of_initial (c,_) =
+ Util.Intset.elements (Evarutil.evars_of_term c)
+ in
+ List.flatten (List.map evars_of_initial initial)
+
let instantiate_evar n com pv =
let (evk,_) =
let evl = Evarutil.non_instantiated pv.solution in
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 25a58a482a..24da9d77b3 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -200,6 +200,9 @@ module V82 : sig
val goals : proofview -> Goal.goal list Evd.sigma
val top_goals : proofview -> Goal.goal list Evd.sigma
+
+ (* returns the existential variable used to start the proof *)
+ val top_evars : proofview -> Evd.evar list
(* Implements the Existential command *)
val instantiate_evar : int -> Topconstr.constr_expr -> proofview -> proofview
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 05:56:53 +0000