Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | | Univs: more robust Universe/Constraint decls #4816 | 2016-06-13 | ||
| | | | * | Univs: fix for part #2 of bug #4816. | 2016-06-13 | ||
* | | | | | Merge branch 'v8.5' | 2016-06-09 | ||
|\ \ \ \ \ | | |_|_|/ | |/| | | | ||||
| | * | | | LtacProf for Coq trunk | 2016-06-05 | ||
| |/ / / |/| | | | ||||
| * | | | Fix incorrect checking of library checksums. | 2016-06-05 | ||
* | | | | Feedback cleanup | 2016-05-31 | ||
| | * | | coqc: support -o option to specify output file name | 2016-05-19 | ||
| |/ / |/| | | ||||
* | | | Dyn: simplify API introducing an Easy submodule | 2016-05-13 | ||
* | | | Merge branch 'v8.5' | 2016-05-09 | ||
|\| | | ||||
| * | | Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module. | 2016-05-08 | ||
* | | | Merge branch 'v8.5' | 2016-05-04 | ||
|\| | | ||||
| * | | Fix bug #4292: Unexpected functor objects. | 2016-05-03 | ||
* | | | Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi... | 2016-04-04 | ||
|\ \ \ | ||||
* \ \ \ | Merge branch 'v8.5' | 2016-03-05 | ||
|\ \ \ \ | | |/ / | |/| | | ||||
| * | | | Fix #4607: do not read native code files if native compiler was disabled. | 2016-03-04 | ||
* | | | | merging conflicts with the original "trunk__CLEANUP__Context__2" branch | 2016-02-15 | ||
|\ \ \ \ | ||||
* \ \ \ \ | Merge branch 'v8.5' | 2016-02-13 | ||
|\ \ \ \ \ | | |/ / / | |/| | | | ||||
| | * | | | CLEANUP: Context.{Rel,Named}.Declaration.t | 2016-02-09 | ||
| |/ / / |/| | | | ||||
| * | | | Optimizing the universes_of_constr_function. | 2016-02-03 | ||
* | | | | Merge branch 'v8.5' | 2016-01-29 | ||
|\| | | | ||||
| * | | | Fix bug #4503: mixing universe polymorphic and monomorphic | 2016-01-23 | ||
* | | | | Merge branch 'v8.5' | 2016-01-21 | ||
|\| | | | ||||
| * | | | Update copyright headers. | 2016-01-20 | ||
| * | | | Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. | 2016-01-15 | ||
* | | | | Changing "P is assumed" to "P is declared". | 2016-01-14 | ||
* | | | | merge | 2016-01-11 | ||
|\ \ \ \ | ||||
| * | | | | CLEANUP: kernel/context.ml{,i} | 2016-01-11 | ||
* | | | | | Merge remote-tracking branch 'origin/v8.5' into trunk | 2016-01-06 | ||
|\ \ \ \ \ | | |/ / / | |/| | | | ||||
| * | | | | Protect code against changes in Map interface. | 2016-01-06 | ||
* | | | | | Remove some unused functions. | 2016-01-02 | ||
* | | | | | Remove keys for evar and meta, since they cannot occur. | 2016-01-02 | ||
* | | | | | Remove some useless type declarations. | 2016-01-02 | ||
* | | | | | Remove Library.mem, which is pointless since 8.5. | 2015-12-31 | ||
* | | | | | Avoid a pointless conversion/copy. | 2015-12-22 | ||
* | | | | | Do not compose "str" and "to_string" whenever possible. | 2015-12-22 | ||
* | | | | | Move the From logic to Loadpath.expand_path. | 2015-12-22 | ||
* | | | | | Do not query module files that have already been loaded. | 2015-12-22 | ||
| |/ / / |/| | | | ||||
* | | | | COMMENTS: added to some variants of "Globalnames.global_reference" type. | 2015-12-18 | ||
* | | | | Merge branch 'v8.5' | 2015-12-08 | ||
|\| | | | ||||
* | | | | Leveraging GADTs to provide a better Dyn API. | 2015-12-05 | ||
* | | | | Specializing the Dyn module to each usecase. | 2015-12-04 | ||
| * | | | Univs: fix bug #4443. | 2015-12-03 | ||
* | | | | Merge branch 'v8.5' | 2015-11-29 | ||
|\| | | | ||||
| * | | | Univs: entirely disallow instantiation of polymorphic constants with | 2015-11-27 | ||
| * | | | Avoid recording spurious Set <= Top.i constraints which are always | 2015-11-27 | ||
* | | | | More efficient implementation of equality-up-to-universes in Universes. | 2015-11-26 | ||
* | | | | Merge branch 'v8.5' | 2015-11-26 | ||
|\| | | | ||||
* | | | | More invariants in UState. | 2015-11-26 | ||
| * | | | Univs: fix type_of_global_in_context not returning instantiated universe cont... | 2015-11-20 | ||
* | | | | Merge branch 'v8.5' | 2015-10-30 | ||
|\| | | |