aboutsummaryrefslogtreecommitdiffstats
path: root/MenhirLib
Commit message (Expand)AuthorAgeFilesLines
* Synchronize vendored MenhirLib with upstream (#416)Jacques-Henri Jourdan2021-10-037-36/+47
* Vendored MenhirLib: replace Require Omega with Require ZArithXavier Leroy2021-09-251-1/+1
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-212-7/+7
* Do not use "Declare Scope", introduced in Coq 8.10 onlyXavier Leroy2020-05-041-1/+0
* Coq-MenhirLib: explicit import ListNotations (#354)Jacques-Henri Jourdan2020-05-047-4/+12
* Fix compatibility with Coq 8.10 (#303)Jacques-Henri Jourdan2019-07-063-9/+10
* New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-0510-0/+2807