aboutsummaryrefslogtreecommitdiff
path: root/vernac/obligations.ml
AgeCommit message (Expand)Author
2017-06-16Clean up universes of constants and inductivesAmin Timany
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-30Support for using type information to infer more precise evar sources.Hugo Herbelin
2017-05-27[coqlib] Deprecate redundant Coqlib functions.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-20Merge PR#627: Obligations shrinking: shrink abstraction tooMaxime Dénès
2017-05-13Uniformity of style for selecting plural or not; spacing for comma.Hugo Herbelin
2017-05-11Obligations shrinking: shrink abstraction tooMatthieu Sozeau
2017-05-01More consistent writing of de Bruijn.Théo Zimmermann
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-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-02-15Make Obligations see fix_exnEnrico Tassi
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-03-02 16:39:13 +0000