aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* 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
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\| |
| * | Fix bug #4292: Unexpected functor objects.Gravatar Pierre-Marie Pédrot2016-05-03
* | | Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...Gravatar Matthieu Sozeau2016-04-04
|\ \ \
* \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\ \ \ \ | | |/ / | |/| |
| * | | Fix #4607: do not read native code files if native compiler was disabled.Gravatar Maxime Dénès2016-03-04
* | | | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \ \ \
* \ \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \ \ \ \ | | |/ / / | |/| | |
| | * | | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ / / |/| | |
| * | | Optimizing the universes_of_constr_function.Gravatar Pierre-Marie Pédrot2016-02-03
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\| | |