diff options
| author |  courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-19 13:09:22 +0000 |
|---|---|---|
| committer | courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-19 13:09:22 +0000 |
| commit | 371388d58ba1d5e3c42fe0f3d5106c97135a1ff1 (patch) | |
| tree | 6971733d3b445c36916ba310f14006364727544f | |
| parent | dadfbd96378d4c1b794ffc341bd10cc4d63b225d (diff) | |
Fixed some printing details for dependent evars in emacs mode. Patch
from Hendrik Tews:
1) Print the dependent evars after "No more subgoals" and after
"No more subgoals but non-instantiated existential". This is
necessary to correctly display the instantiation status of dependent
evars, because the last proof command might change them.
2) Change the ``Show Goal "id"'' command to include a header like
goal / evar 2 is:
This is more consistent with the other Show commands. Moreover it
simplifies the use of this command in Proof General, because, with
the change, the output contains the goal ID.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14824 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/printer.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 919ec188b..0b9ce9188 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -357,11 +357,13 @@ let default_pr_subgoals close_cmd sigma seeds = function | None -> let exl = Evarutil.non_instantiated sigma in if exl = [] then - (str"No more subgoals." ++ fnl ()) + (str"No more subgoals." ++ fnl () + ++ emacs_print_dependent_evars sigma seeds) else let pei = pr_evars_int 1 exl in (str "No more subgoals but non-instantiated existential " ++ - str "variables:" ++ fnl () ++ (hov 0 pei)) + str "variables:" ++ fnl () ++ (hov 0 pei) + ++ emacs_print_dependent_evars sigma seeds) end | [g] -> let pg = default_pr_goal { it = g ; sigma = sigma } in @@ -442,8 +444,12 @@ let pr_nth_open_subgoal n = let pr_goal_by_id id = let p = Proof_global.give_me_the_proof () in let g = Goal.get_by_uid id in + let pr gs = + v 0 (str ("goal / evar " ^ id ^ " is:") ++ cut () + ++ pr_goal gs) + in try - Proof.in_proof p (fun sigma -> pr_goal {it=g;sigma=sigma}) + Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma}) with Not_found -> error "Invalid goal identifier." (* Elementary tactics *) |