diff options
| author | Tej Chajed | 2020-02-10 18:19:45 -0500 |
|---|---|---|
| committer | Tej Chajed | 2020-02-10 18:19:45 -0500 |
| commit | 481db1ce8b0e653c22f332ef7eab5c1fa575b6f4 (patch) | |
| tree | 7283d837a8f17e2c0b6604a26e3c8ccf58eb6093 /kernel/typeops.ml | |
| parent | 056c66fef0def03c495b17b54dd3ff5c706337a4 (diff) | |
Recognize Default Proof Using in STM
Treat a Set Default Proof Using call the same as having a syntactic
Proof using ... annotation. This ensures that proofs in sections are
skipped in -vos mode when there are enough annotations to determine the
type of the resulting theorem.
Fixes #11342.
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions