aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Fix various shortcomings of the warnings infrastructure.Gravatar Maxime Dénès2016-11-02
* Put string between quotes when printing an option value.Gravatar Maxime Dénès2016-11-02
* Merge remote-tracking branch 'github/pr/337' into v8.6Gravatar Maxime Dénès2016-10-28
|\
| * Add missing dot to impargs error message.Gravatar Maxime Dénès2016-10-27
| * Proper fix for #3753 (anomaly with implicit arguments and renamings)Gravatar Maxime Dénès2016-10-27
| * Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
* | Cleanup code according to comments.Gravatar Matthieu Sozeau2016-10-20
* | Fix minimization to be insensitive to redundant arcs.Gravatar Matthieu Sozeau2016-10-20
* | Merge branch 'bug5036' into v8.6Gravatar Matthieu Sozeau2016-10-20
|\ \ | |/ |/|
| * Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-10-20
* | Fix a bug of Mltop.declare_cache_object.Gravatar Pierre-Marie Pédrot2016-10-05
* | Changing the separator for appended string options to comma.Gravatar Maxime Dénès2016-10-04
* | Allow appending to string options.Gravatar Guillaume Melquiond2016-10-01
* | Merge remote-tracking branch 'github/pr/299' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \
* | | Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-09-29
| |/ |/|
| * Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
|/
* Fix bug #5090: Effect of -Q depends on coqtop's current directory.Gravatar Pierre-Marie Pédrot2016-09-25
* Remove dead code in library/lib.ml.Gravatar Maxime Dénès2016-09-20
* A proposal to unify the messages given by Test and Print Options (#5062).Gravatar Hugo Herbelin2016-09-06
* Summary: simpler API for process-local storageGravatar Enrico Tassi2016-09-05
* Emit a warning on Require inside a module.Gravatar Maxime Dénès2016-08-30
* Send Dependency feedback only if file not already loaded.Gravatar Maxime Dénès2016-08-29
* Fix bug #4750: Change format of inconsistent assumptions message.Gravatar Pierre-Marie Pédrot2016-08-28
* More standard naming for the Imparg.with_implicits function.Gravatar Pierre-Marie Pédrot2016-08-20
* Removing dead code in Impargs.Gravatar Pierre-Marie Pédrot2016-08-19
* COMMENT: moving misplaced comment where it belongsGravatar Matej Kosik2016-07-29
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Exporting section_segment_of_reference.Gravatar Hugo Herbelin2016-06-29
* universes.ml: Minor code cleanupGravatar Matthieu Sozeau2016-06-29
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\
* | Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* | Adding a local type-in-type flag in kernel declarations.Gravatar Pierre-Marie Pédrot2016-06-18
* | Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
| * | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | | Merge remote-tracking branch 'origin/pr/166' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \
* \ \ \ Merge branch "LtacProf for trunk" (PR #165).Gravatar Pierre-Marie Pédrot2016-06-14
|\ \ \ \
* | | | | Univs: more robust Universe/Constraint decls #4816Gravatar Matthieu Sozeau2016-06-13
| | | | * Univs: fix for part #2 of bug #4816.Gravatar Matthieu Sozeau2016-06-13
* | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\ \ \ \ \ | | |_|_|/ | |/| | |
| | * | | LtacProf for Coq trunkGravatar Jason Gross2016-06-05
| |/ / / |/| | |
| * | | Fix incorrect checking of library checksums.Gravatar Maxime Dénès2016-06-05
* | | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | * | coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
| |/ / |/| |
* | | Dyn: simplify API introducing an Easy submoduleGravatar Enrico Tassi2016-05-13
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\| |
| * | Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.Gravatar Pierre-Marie Pédrot2016-05-08