| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-11-24 | `in11(1)_sig` subsumes `in(2|3)_sig` | Kazuhiko Sakaguchi | |
| 2020-11-24 | factoring out in_sig | Cyril Cohen | |
| 2020-11-01 | minimizing variables | Cyril Cohen | |
| Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com> | |||
| 2020-11-01 | generic interactions between in and on | Cyril Cohen | |
| + Taking into account Kazuhiko's remarks Co-authored-by: Kazuhiko Sakaguchi <sakaguchi@coins.tsukuba.ac.jp> | |||
| 2020-08-11 | fix notation-incompatible-format warnings | Christian Doczkal | |
| 2020-06-17 | contra lemmas involving propositions | Christian Doczkal | |
| 2020-06-08 | Documenting addition policy to coq. | Cyril Cohen | |
| 2020-06-06 | bugfix | Cyril Cohen | |
| 2020-06-06 | Missing homo_mono lemmas | Cyril Cohen | |
| 2020-06-05 | Missing mono lemmas (#513) | Cyril Cohen | |
| * Missing mono lemmas | |||
| 2019-05-06 | add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma names | Georges Gonthier | |
| - add notation support for lemma renaming PRs, helping clients adjust to the name change by emitting warning or raising errors when the old name is used. The default is to emit warnings, but clients can change this to silence (if electing to delay migration) or errors (to help with actual migration). Usage: Notation old_id := (deprecate old_id new_id) (only parsing). —> Caveat 1: only prenex maximal implicit of `new_id` are preserved, so, as `Notation` does not support on-demand implicits, the latter should be added explicitly as in `(deprecate old new _ _)`. —> Caveat 2: the warnings are emitted by a tactic-in-term, which is interpreted during type elaboration. As the SSReflect elaborator may re-infer type in arguments multiple times (notably, views and arguments to `apply` and `rewrite`), clients may see duplicate warnings. - use the `deprecate` facility to introduce the first part of the refactoring of `seq` permutation lemmas : only lemmas concerning `perm_eq` should have `perm` as a component of their name. - document local additions in `ssreflect.v` and `ssrbool.v` - add 8.8 `odd-order` regression - the explicit beta-redex idiom use in the `perm_uniq` and `leq_min_perm` aliases avoids a strange name-sensitive bug of view interpretation in Coq 8.7. | |||
| 2019-04-29 | Generalise use of `{pred T}` from coq/coq#9995 | Georges Gonthier | |
| Use `{pred T}` systematically for generic _collective_ boolean predicate. Use `PredType` to construct `predType` instances. Instrument core `ssreflect` files to replicate these and other new features introduces by coq/coq#9555 (`nonPropType` interface, `simpl_rel` that simplifies with `inE`). | |||
| 2017-06-07 | For trunk, use merged ssr plugin. | Maxime Dénès | |
| 2016-12-20 | correct a typo in the documentation | Yves Bertot | |
| 2016-11-07 | update copyright banner | Assia Mahboubi | |
| 2016-04-08 | Fixing compilation after the merge of PR trunk-function_scope. | Pierre-Marie Pédrot | |
| 2015-11-30 | Typos in comments. | Assia Mahboubi | |
| 2015-11-20 | Typo. | Assia Mahboubi | |
| 2015-11-20 | Typos | Assia Mahboubi | |
| 2015-07-28 | update copyright banner | Enrico Tassi | |
| 2015-07-17 | Updating files + reorganizing everything | Cyril Cohen | |
| 2015-03-09 | Initial commit | Enrico Tassi | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |