aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-21[flags] Deprecate is_silent/is_verbose in favor of single flag.Emilio Jesus Gallego Arias
2017-04-06Fix a normalization hotspot in computation of constr keys.Pierre-Marie Pédrot
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24[nit] Fix a couple incorrect uses of msg_error.Emilio Jesus Gallego Arias
2017-03-22Merge PR#390: Updates to the Pretty Printing InfrastructureMaxime Dénès
2017-03-22Merge PR#478: Small optimization on handling of library state.Maxime Dénès
2017-03-21[pp] [ide] Minor cleanups in pp code.Emilio Jesus Gallego Arias
2017-03-21[error] Move back fatal_error to toplevelEmilio Jesus Gallego Arias
2017-03-14[safe_string] library/nameopsEmilio Jesus Gallego Arias
2017-03-14[library] Refactor state handling.Emilio Jesus Gallego Arias
2017-03-14[library] Don't recompute path_prefix on unfreeze.Emilio Jesus Gallego Arias
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
2016-12-19Use Pp.quote in string options.Maxime Dénès
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-02Fix various shortcomings of the warnings infrastructure.Maxime Dénès
2016-11-02Put string between quotes when printing an option value.Maxime Dénès
2016-10-30Moving Universes to the engine/ folder.Pierre-Marie Pédrot
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-28Merge remote-tracking branch 'github/pr/337' into v8.6Maxime Dénès
2016-10-27Add missing dot to impargs error message.Maxime Dénès
2016-10-27Proper fix for #3753 (anomaly with implicit arguments and renamings)Maxime Dénès
2016-10-27Complete overhaul of the Arguments vernacular.Maxime Dénès
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-20Cleanup code according to comments.Matthieu Sozeau
2016-10-20Fix minimization to be insensitive to redundant arcs.Matthieu Sozeau
2016-10-20Merge branch 'bug5036' into v8.6Matthieu Sozeau
2016-10-20Fix bug #5036 autorewrite, sections and universesMatthieu Sozeau
2016-10-19COMMENT: was added to "Nameops.increment_suffix".Matej Kosik
2016-10-19CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Matej Kosik
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-05Fix a bug of Mltop.declare_cache_object.Pierre-Marie Pédrot
2016-10-04Changing the separator for appended string options to comma.Maxime Dénès
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-01Allow appending to string options.Guillaume Melquiond
2016-09-30Merge remote-tracking branch 'github/pr/299' into v8.6Maxime Dénès
2016-09-29Fix bug #5036 autorewrite, sections and universesMatthieu Sozeau
2016-09-29Fix bug #4869, allow Prop, Set, and level names in constraints.Matthieu Sozeau
2016-09-27Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-25Fix bug #5090: Effect of -Q depends on coqtop's current directory.Pierre-Marie Pédrot
2016-09-23Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
2016-09-20Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Maxime Dénès
2016-09-20Stylistic improvements in intf/decl_kinds.mli.Maxime Dénès
2016-09-20Remove dead code in library/lib.ml.Maxime Dénès
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-09-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-06A proposal to unify the messages given by Test and Print Options (#5062).Hugo Herbelin