diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/name_mangling.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/name_mangling.v b/test-suite/success/name_mangling.v index e84d221d59..d99e407b0d 100644 --- a/test-suite/success/name_mangling.v +++ b/test-suite/success/name_mangling.v @@ -69,7 +69,7 @@ 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 *) @@ -109,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. |