aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/obligations.ml
Commit message (Expand)AuthorAge
* [coqlib] Deprecate redundant Coqlib functions.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/
| * Merge PR#627: Obligations shrinking: shrink abstraction tooGravatar Maxime Dénès2017-05-20
| |\
| * | Uniformity of style for selecting plural or not; spacing for comma.Gravatar Hugo Herbelin2017-05-13
| | * Obligations shrinking: shrink abstraction tooGravatar Matthieu Sozeau2017-05-11
| |/
| * More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
* Make Obligations see fix_exnGravatar Enrico Tassi2017-02-15
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15