aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/lemmas.ml
Commit message (Expand)AuthorAge
* Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
|\
| * 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