diff options
| author | Hugo Herbelin | 2020-05-10 22:54:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-14 12:21:30 +0200 |
| commit | cd1bb55339040bc272a9a752703e259e27ddbcd4 (patch) | |
| tree | d7628e94b5364ee9678b5b6ba1793450e5e613cc | |
| parent | 6f2b88649ec0c1e27befe7bcd2cdbec0ccee95d6 (diff) | |
Fixes #12234 (wrong environment for Show Proof).
We take the env of the current goal with the context replaced with
section variables. In practice, this is the global env, but, maybe,
one day, a goal state will have its own env.
| -rw-r--r-- | test-suite/bugs/closed/bug_12234.v | 9 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 8 |
2 files changed, 16 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_12234.v b/test-suite/bugs/closed/bug_12234.v new file mode 100644 index 0000000000..b99c5d524e --- /dev/null +++ b/test-suite/bugs/closed/bug_12234.v @@ -0,0 +1,9 @@ +(* Checking a Show Proof bug *) +Section S. +Variable A:Prop. +Theorem thm (a:A) : True. +assert (b:=a). +clear A a b. +Show Proof. +Abort. +End S. diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index aac0b54ed4..6568d7bf14 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -95,8 +95,14 @@ let show_proof ~pstate = try let pstate = Option.get pstate in let p = Declare.Proof.get_proof pstate in - let sigma, env = Declare.get_current_context pstate in + let sigma, _ = Declare.get_current_context pstate in let pprf = Proof.partial_proof p in + (* In the absence of an environment explicitly attached to the + proof and on top of which side effects of the proof would be pushed, , + we take the global environment which in practise should be a + superset of the initial environment in which the proof was + started *) + let env = Global.env() in Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf (* We print nothing if there are no goals left *) with |