coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-06-20	Add a pre-hook mechanism for the `zify` tactic	Kazuhiko Sakaguchi

2020-06-14	Update zify documentation	Frédéric Besson
	Add Zify <X> are documented. Add <X> is deprecated as it clashed with the standard Add command
2020-06-14	fix according to review by @pi8027	Frédéric Besson

2020-06-14	Update theories/micromega/ZifyBool.v	Frédéric Besson
	Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com> - insert boolean constraint (b = true \/ b = false) - add specs for b2z - zify_post_hook performs a case-analysis over boolean constraints - Stricter typing constraints for `zify` declared operators The type is syntactically checked against the declaration of injections. Some explicit casts may need to be inserted.
2020-06-14	[micromega] native support for boolean operators	Frédéric Besson
	The syntax of formulae is extended to support boolean constants (true, false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb, Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and Z.ltb.
2020-05-09	Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.	Maxime Dénès
	Reviewed-by: maximedenes
2020-04-30	[zify] add support for Nat.le, Nat.lt and Nat.eq	Frédéric Besson
	Nat.le, Nat.lt and Nat.eq are aliased to le, lt and @eq nat. The required declarations are now added in ZifyInst.
2020-04-17	ZArith: move lia hints to a dedicated module	Vincent Laporte

2020-04-03	Avoiding using a fixed introduction name in Ltac code of stdlib.	Hugo Herbelin

2020-04-01	[micromega] use Coqlib.lib_ref to get Coq constants.	Frédéric Besson

2020-03-21	Add module ZifyPow to avoid compatibility issue with 8.11.	Théo Zimmermann
	Also tweak the changelog entry to explain the difference.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-03-03	[zify] efficiency improvements	Frédéric Besson
	- zify_iter_specs is entirely in OCaml - zify_op has been improved * The generation of proof-terms is more direct * It does not `rewrite` but instead either performs a `pose proof` or a `change` * The support for `and`, `or`, `not`, arrow is hardcoded * Avoid generating duplicate hypotheses such as 0 <= Z.of_nat x - zify_elim_let is entirely in OCaml (no Ltac callback) [micromega] fix stack overflow Less naive computation of bounds (online elimination of duplicates)
2020-02-13	[build] Consolidate stdlib's .v files under a single directory.	Emilio Jesus Gallego Arias
	Currently, `.v` under the `Coq.` prefix are found in both `theories` and `plugins`. Usually these two directories are merged by special loadpath code that allows double-binding of the prefix. This adds some complexity to the build and loadpath system; and in particular, it prevents from handling the `Coq.*` prefix in the simple, `-R theories Coq` standard way. We thus move all `.v` files to theories, leaving `plugins` as an OCaml-only directory, and modify accordingly the loadpath / build infrastructure. Note that in general `plugins/foo/Foo.v` was not self-contained, in the sense that it depended on files in `theories` and files in `theories` depended on it; moreover, Coq saw all these files as belonging to the same namespace so it didn't really care where they lived. This could also imply a performance gain as we now effectively traverse less directories when locating a library. See also discussion in #10003