https://github.com/EasyCrypt/easycrypt
Revision c2523f32e7a3ba6b2f8c9ec82c5d63be837615e5 authored by Pierre-Yves Strub on 28 July 2015, 11:13:31 UTC, committed by Pierre-Yves Strub on 28 July 2015, 11:13:31 UTC
Axioms can now be tagged with a set of symbols. The syntax is:

  `axiom [tag1 tag2...]? nosmt? name : spec.`

In theory cloning, catch-all proof specification can be also tagged.
The syntax is:

  `clone ... proof T.* [tag1 tag2...]?`

The proof specification is then only applied to axioms whose tags
have a non-empty intersection with the proof specification tags.
(If no tags are provided, the old behavior is obtained - i.e. the
proof specification is applied unconditionally).

It is now allowed to give multiple starred proof-specifications. If so,
the first proof-specification matching is applied.

[close #17165]
1 parent 96e855d
History
Tip revision: c2523f32e7a3ba6b2f8c9ec82c5d63be837615e5 authored by Pierre-Yves Strub on 28 July 2015, 11:13:31 UTC
axiom can now be tagged for better proof specification in cloning.
Tip revision: c2523f3
File Mode Size
config
examples
lint
packaging
proofgeneral
scripts
src
system
tests
theories
.gitignore -rw-r--r-- 450 bytes
.merlin -rw-r--r-- 208 bytes
COPYRIGHT -rw-r--r-- 465 bytes
MANIFEST -rw-r--r-- 1.1 KB
Makefile -rw-r--r-- 5.8 KB
Makefile.system -rw-r--r-- 478 bytes
README.md -rw-r--r-- 9.8 KB
_tags -rw-r--r-- 739 bytes
myocamlbuild.ml -rw-r--r-- 2.3 KB

README.md

back to top