| Age | Commit message (Collapse) | Author |
|---|
|
- rename files to get rid of prefix
- use -Q to get package name right
- add Base.v to make package imports simpler
- add opam file for coq package
|
|
- ArithFact takes a boolean predicate
- defined in terms of ArithFactP, which takes a Prop predicate,
and is used directly for existentials
- used abstract in more definitions with direct proofs
- beef up solve_bool_with_Z to handle more equalities, andb and orb
|
|
Also tweak the informative and/or boolean definitions so that they use
the same proofs in both monads.
|
|
* rename state fields to avoid clash with regstate type
* use rewriting to automate some proofs
|
|
|
|
NB: requires minor changes in the models
|
|
|
