aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching/ssrmatching.ml
Commit message (Collapse)AuthorAge
* Correct some spelling errorsmasterGravatar Benjamin Barenblat2018-07-22
| | | | | | | | | | Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`.
* Split the Ssrmatching module between code and grammar rules.Gravatar Pierre-Marie Pédrot2018-06-30
Fixes #7857.