aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES2
-rw-r--r--parsing/g_proofs.ml46
-rw-r--r--parsing/ppvernac.ml6
-rw-r--r--parsing/printer.ml7
-rw-r--r--parsing/printer.mli1
-rw-r--r--proofs/goal.ml11
-rw-r--r--proofs/goal.mli3
-rw-r--r--proofs/proof.ml3
-rw-r--r--proofs/proof.mli5
-rw-r--r--proofs/proofview.ml6
-rw-r--r--proofs/proofview.mli9
-rw-r--r--toplevel/vernacentries.ml13
-rw-r--r--toplevel/vernacentries.mli2
-rw-r--r--toplevel/vernacexpr.ml9
14 files changed, 71 insertions, 12 deletions
diff --git a/CHANGES b/CHANGES
index 44bbdcb42..540b3fe30 100644
--- a/CHANGES
+++ b/CHANGES
@@ -63,6 +63,8 @@ Vernacular commands
- A new option "Set Default Timeout n / Unset Default Timeout".
- Qed now uses information from the reduction tactics used in proof script
to avoid conversion at Qed time to go into a very long computation.
+- New command "Show Goal ident" to display the statement of a goal, even
+ a closed one (available from Proof General).
Module System
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 3139f5759..0f5d80a83 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -66,8 +66,10 @@ GEXTEND Gram
| IDENT "BeginSubproof" -> VernacSubproof None
| IDENT "BeginSubproof"; n = natural -> VernacSubproof (Some n)
| IDENT "EndSubproof" -> VernacEndSubproof
- | IDENT "Show" -> VernacShow (ShowGoal None)
- | IDENT "Show"; n = natural -> VernacShow (ShowGoal (Some n))
+ | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals)
+ | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n))
+ | IDENT "Show"; IDENT "Goal"; n = string ->
+ VernacShow (ShowGoal (GoalId n))
| IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural ->
VernacShow (ShowGoalImplicitly n)
| IDENT "Show"; IDENT "Node" -> VernacShow ShowNode
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 375e071f8..bb20dc7fc 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -466,8 +466,12 @@ let rec pr_vernac = function
str "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k]
| VernacFocus i -> str"Focus" ++ pr_opt int i
| VernacShow s ->
+ let pr_goal_reference = function
+ | OpenSubgoals -> mt ()
+ | NthGoal n -> spc () ++ int n
+ | GoalId n -> spc () ++ str n in
let pr_showable = function
- | ShowGoal n -> str"Show" ++ pr_opt int n
+ | ShowGoal n -> str"Show" ++ pr_goal_reference n
| ShowGoalImplicitly n -> str"Show Implicit Arguments" ++ pr_opt int n
| ShowProof -> str"Show Proof"
| ShowNode -> str"Show Node"
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 046d55ae3..232551984 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -403,6 +403,13 @@ let pr_nth_open_subgoal n =
let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
pr_subgoal n sigma gls
+let pr_goal_by_id id =
+ let p = Proof_global.give_me_the_proof () in
+ let g = Goal.get_by_uid id in
+ try
+ Proof.in_proof p (fun sigma -> pr_goal {it=g;sigma=sigma})
+ with Not_found -> error "Invalid goal identifier."
+
(* Elementary tactics *)
let pr_prim_rule = function
diff --git a/parsing/printer.mli b/parsing/printer.mli
index cdd2f4277..b7e581cd5 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -136,6 +136,7 @@ val prterm : constr -> std_ppcmds (** = pr_lconstr *)
It is used primarily by the Print Assumption command. *)
val pr_assumptionset : env -> Term.types Environ.ContextObjectMap.t ->std_ppcmds
+val pr_goal_by_id : string -> std_ppcmds
type printer_pr = {
pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds;
diff --git a/proofs/goal.ml b/proofs/goal.ml
index b2e05a524..b50177eea 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -23,7 +23,6 @@ type goal = {
(* spiwack: I don't deal with the tags, yet. It is a worthy discussion
whether we do want some tags displayed besides the goal or not. *)
-let uid {content = e} = string_of_int e
let pr_goal {content = e} = str "GOAL:" ++ Pp.int e
@@ -38,6 +37,16 @@ let build e =
tags = []
}
+
+let uid {content = e} = string_of_int e
+let get_by_uid u =
+ (* this necessarily forget about tags.
+ when tags are to be implemented, they
+ should be done another way.
+ We could use the store in evar_extra,
+ for instance. *)
+ build (int_of_string u)
+
(* Builds a new goal with content evar [e] and
inheriting from goal [gl]*)
let descendent gl e =
diff --git a/proofs/goal.mli b/proofs/goal.mli
index c36b359ed..e9d230659 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -18,6 +18,9 @@ val build : Evd.evar -> goal
(* Gives a unique identifier to each goal. The identifier is
guaranteed to contain no space. *)
val uid : goal -> string
+(* Returns the goal (even if it has been partially solved)
+ corresponding to a unique identifier obtained by {!uid}. *)
+val get_by_uid : string -> goal
(* Debugging help *)
val pr_goal : goal -> Pp.std_ppcmds
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 23ce2c8eb..828365798 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -410,7 +410,10 @@ let run_tactic env tac pr =
restore_state starting_point pr;
raise e
+(*** Commands ***)
+let in_proof p k =
+ Proofview.in_proofview p.state.proofview k
(*** Compatibility layer with <=v8.2 ***)
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 7de0a9fdf..b4c84cbf6 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -154,6 +154,11 @@ val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> unit
[transaction p f] can be called on an [f] using, itself, [transaction p].*)
val transaction : proof -> (unit -> unit) -> unit
+
+(*** Commands ***)
+
+val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a
+
(*** Compatibility layer with <=v8.2 ***)
module V82 : sig
val subgoals : proof -> Goal.goal list Evd.sigma
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 3964692b1..b76c802df 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -433,6 +433,12 @@ let tclSENSITIVE s =
fun env -> { go = fun sk fk step -> sk () fk (sensitive_on_step s env step) }
end
+
+(*** Commands ***)
+
+let in_proofview p k =
+ k p.solution
+
module Notations = struct
let (>-) = Goal.bind
let (>>-) = tclGOALBINDU
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index e8cf7d26d..25a58a482 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -153,6 +153,15 @@ val tclGOALBINDU : 'a Goal.sensitive -> ('a -> unit tactic) -> unit tactic
(* [tclSENSITIVE] views goal-type tactics as a special kind of tactics.*)
val tclSENSITIVE : Goal.subgoals Goal.sensitive -> unit tactic
+
+(*** Commands ***)
+
+val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a
+
+
+
+
+
(* Notations for building tactics. *)
module Notations : sig
(* Goal.bind *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1b25fb926..2b298f2ac 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -45,7 +45,7 @@ type pcoq_hook = {
print_check : Environ.env -> Environ.unsafe_judgment -> unit;
print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr ->
Environ.unsafe_judgment -> unit;
- show_goal : int option -> unit
+ show_goal : goal_reference -> unit
}
let pcoq = ref None
@@ -1259,11 +1259,12 @@ let vernac_end_subproof () =
Proof.unfocus subproof_kind p ; print_subgoals ()
let vernac_show = function
- | ShowGoal nopt ->
- if !pcoq <> None then (Option.get !pcoq).show_goal nopt
- else msg (match nopt with
- | None -> pr_open_subgoals ()
- | Some n -> pr_nth_open_subgoal n)
+ | ShowGoal goalref ->
+ if !pcoq <> None then (Option.get !pcoq).show_goal goalref
+ else msg (match goalref with
+ | OpenSubgoals -> pr_open_subgoals ()
+ | NthGoal n -> pr_nth_open_subgoal n
+ | GoalId id -> pr_goal_by_id id)
| ShowGoalImplicitly None ->
Constrextern.with_implicits msg (pr_open_subgoals ())
| ShowGoalImplicitly (Some n) ->
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 814676575..8fb6f4668 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -39,7 +39,7 @@ type pcoq_hook = {
print_check : Environ.env -> Environ.unsafe_judgment -> unit;
print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr ->
Environ.unsafe_judgment -> unit;
- show_goal : int option -> unit
+ show_goal : goal_reference -> unit
}
val set_pcoq_hook : pcoq_hook -> unit
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 6ea4e263f..a6c304f67 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -31,6 +31,13 @@ type lreference = reference
type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
+type goal_identifier = string
+
+type goal_reference =
+ | OpenSubgoals
+ | NthGoal of int
+ | GoalId of goal_identifier
+
type printable =
| PrintTables
| PrintFullContext
@@ -83,7 +90,7 @@ type locatable =
| LocateFile of string
type showable =
- | ShowGoal of int option
+ | ShowGoal of goal_reference
| ShowGoalImplicitly of int option
| ShowProof
| ShowNode
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 11:48:19 +0000