aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/lemmas.ml
Commit message (Expand)AuthorAge
* [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Don't double up on periods in anomaliesGravatar Jason Gross2017-06-02
* [cleanup] Unify all calls to the error function.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
| * | [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| |/
| * Fix two new unused opens.Gravatar Maxime Dénès2017-05-02
| * Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
| |\
* | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/ /
| * Fixing #5420 as well as many related bugs due to miscounting let-ins.Gravatar Hugo Herbelin2017-04-09
| * Fixing several wrong computations of implicit arguments by positionGravatar Hugo Herbelin2017-04-09
| * Removing internal support for accepting "{struct x}" and co in "Theorem with".Gravatar Hugo Herbelin2017-04-09
* | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\|
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
|/
* [future] Remove unused parameter greedy.Gravatar Emilio Jesus Gallego Arias2017-03-14
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15