diff options
| author | Gaëtan Gilbert | 2020-08-28 15:38:04 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-28 16:31:09 +0200 |
| commit | 2269c97be12263f96a538c1c5311b78b3eb67915 (patch) | |
| tree | 9c9c20b6e354e9707ae9381fd420d271f8062a03 | |
| parent | 4341759b033286b132ecaeb4816db63c47a66e10 (diff) | |
Name saved goals in name_mangling test
Should be more robust with async proofs
| -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. |