aboutsummaryrefslogtreecommitdiff
path: root/vernac/lemmas.ml
AgeCommit message (Expand)Author
2017-07-13Removing the uses of abstraction-breaking code in Lemmas.Pierre-Marie Pédrot
2017-07-13Safer API for Global.body_of_constant and variants.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-02Don't double up on periods in anomaliesJason Gross
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-25Merge PR#481: [option] Remove support for non-synchronous options.Maxime Dénès
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-05-23[vernac] Remove `Save thm id.` command.Emilio Jesus Gallego Arias
2017-05-02Fix two new unused opens.Maxime Dénès
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Maxime Dénès
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-09Fixing #5420 as well as many related bugs due to miscounting let-ins.Hugo Herbelin
2017-04-09Fixing several wrong computations of implicit arguments by positionHugo Herbelin
2017-04-09Removing internal support for accepting "{struct x}" and co in "Theorem with".Hugo Herbelin
2017-04-07Merge branch 'master' into econstrPierre-Marie Pédrot
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-23Ensuring static invariants about handling of pending evars in Pretyping.Pierre-Marie Pédrot
2017-03-14[future] Remove unused parameter greedy.Emilio Jesus Gallego Arias
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 13:39:39 +0000