diff options
| author | Pierre-Marie Pédrot | 2020-08-29 20:09:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-29 20:09:20 +0200 |
| commit | fd8da75905aac60d9c38eb0369a3cd10081ce586 (patch) | |
| tree | b5cc832da457d24b69f07d7204e7e0d0471abe57 /test-suite/success | |
| parent | 94115a6c760a69f5a9730f48410af98e822336b8 (diff) | |
| parent | 2269c97be12263f96a538c1c5311b78b3eb67915 (diff) | |
Merge PR #12929: Make abstract compatible with mangle names
Reviewed-by: jashug
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/name_mangling.v | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/test-suite/success/name_mangling.v b/test-suite/success/name_mangling.v index e982414206..d99e407b0d 100644 --- a/test-suite/success/name_mangling.v +++ b/test-suite/success/name_mangling.v @@ -1,7 +1,6 @@ -(* -*- coq-prog-args: ("-mangle-names" "_") -*- *) +Set Mangle Names. (* Check that refine policy of redefining previous names make these names private *) -(* abstract can change names in the environment! See bug #3146 *) Goal True -> True. intro. @@ -58,7 +57,7 @@ Abort. Goal False -> False. intro H. -Fail abstract exact H. +abstract exact H. Abort. (* Variant *) @@ -70,12 +69,11 @@ Abort. (* Example from Jason *) -Goal False -> False. +Lemma lem1 : False -> False. intro H. (* Name H' is from Ltac here, so it preserves the privacy *) (* But abstract messes everything up *) -Fail let H' := H in abstract exact H'. -let H' := H in exact H'. +let H' := H in abstract exact H'. Qed. (* Variant *) @@ -111,7 +109,7 @@ Goal forall b : False, b = b. Fail destruct b0. Abort. -Goal forall b : False, b = b. +Lemma lem2 : forall b : False, b = b. now destruct b. Qed. End foo. |