| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-04-16 | [zify] bugfix | Frederic Besson | |
| - to zify the conclusion, we are using Tactics.apply (not rewrite) Closes #11089 - constrain the arguments of Add Zify X to be GlobRef.t Unset Primitive Projections so that projections are GlobRef.t. Closes #14043 Update doc/sphinx/addendum/micromega.rst Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> | |||
| 2020-06-20 | Add a pre-hook mechanism for the `zify` tactic | Kazuhiko Sakaguchi | |
| 2020-06-14 | fix according to review by @pi8027 | Frédéric Besson | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |