| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-10-23 | Move bug files to match their new GitHub ID (fixes #6001). | Théo Zimmermann | |
| 2017-10-05 | Omega now aware of context variables with bodies (in type Z or nat) (fix bug ↵ | Pierre Letouzey | |
| 148) For compatibility, this extra feature of omega could be disabled via Unset Omega UseLocalDefs. Caveat : for now, real let-ins inside goals or hyps aren't handled, use some "cbv zeta" reduction if you want to get rid of them. And context definitions whose types aren't Z or nat are ignored, some manual "unfold" are still mandatory if expanding these definitions will help omega. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |