Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Validate Proof command: runs typing.ml on the current proof
- Loading branch information
1 parent
4c4c43a
commit 328e47a
Showing
11 changed files
with
90 additions
and
1 deletion.
There are no files selected for viewing
5 changes: 5 additions & 0 deletions
5
doc/changelog/08-vernac-commands-and-options/17467-validate-proof.rst
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
- **Added:** | ||
:cmd:`Validate Proof` runs the type checker on the current proof, | ||
complementary with :cmd:`Guarded` which runs the guard checker. | ||
(`#17467 <https://github.com/coq/coq/pull/17467>`_, | ||
by Gaëtan Gilbert). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
|
||
Module M. | ||
Private Inductive foo := . | ||
|
||
Definition to_nat (f:foo) : nat := match f with end. | ||
End M. | ||
|
||
Lemma bar : False. | ||
Proof. | ||
exact_no_check I. | ||
Fail Validate Proof. | ||
Abort. | ||
|
||
Lemma bar f : M.to_nat f = 0. | ||
Proof. | ||
Validate Proof. | ||
|
||
cbv. | ||
|
||
Fail Validate Proof. | ||
|
||
Abort. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters