aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/vernacexpr.ml
Commit message (Expand)AuthorAge
* Improve errors for cumulativity when monomorphicGravatar Amin Timany2017-07-31
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [vernac] Remove stale bool parameter from `VernacStartTheoremProof`Gravatar Emilio Jesus Gallego Arias2017-06-21
* Merge PR#774: [ide] Add route_id parameter to query call.Gravatar Maxime Dénès2017-06-20
|\
| * [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
* | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
|/
* Remove Show Thesis command which was never implemented.Gravatar Théo Zimmermann2017-06-12
* Remove non-working Show Tree and Show Node commands.Gravatar Théo Zimmermann2017-06-12
* Remove Show Implicit Arguments command.Gravatar Théo Zimmermann2017-06-12
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07