aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-08Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.Pierre-Marie Pédrot
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03Fix bug #4292: Unexpected functor objects.Pierre-Marie Pédrot
2016-04-04Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...Matthieu Sozeau
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-04Fix #4607: do not read native code files if native compiler was disabled.Maxime Dénès
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-02-03Optimizing the universes_of_constr_function.Pierre-Marie Pédrot
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-23Fix bug #4503: mixing universe polymorphic and monomorphicMatthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2016-01-14Changing "P is assumed" to "P is declared".Hugo Herbelin
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-06Merge remote-tracking branch 'origin/v8.5' into trunkGuillaume Melquiond
2016-01-06Protect code against changes in Map interface.Maxime Dénès
2016-01-02Remove some unused functions.Guillaume Melquiond
2016-01-02Remove keys for evar and meta, since they cannot occur.Guillaume Melquiond
2016-01-02Remove some useless type declarations.Guillaume Melquiond
2015-12-31Remove Library.mem, which is pointless since 8.5.Guillaume Melquiond
2015-12-22Avoid a pointless conversion/copy.Guillaume Melquiond
2015-12-22Do not compose "str" and "to_string" whenever possible.Guillaume Melquiond
2015-12-22Move the From logic to Loadpath.expand_path.Guillaume Melquiond
2015-12-22Do not query module files that have already been loaded.Guillaume Melquiond
2015-12-18COMMENTS: added to some variants of "Globalnames.global_reference" type.Matej Kosik
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-05Leveraging GADTs to provide a better Dyn API.Pierre-Marie Pédrot
2015-12-04Specializing the Dyn module to each usecase.Pierre-Marie Pédrot
2015-12-03Univs: fix bug #4443.Matthieu Sozeau
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-11-27Avoid recording spurious Set <= Top.i constraints which are alwaysMatthieu Sozeau
2015-11-26More efficient implementation of equality-up-to-universes in Universes.Pierre-Marie Pédrot
2015-11-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-26More invariants in UState.Pierre-Marie Pédrot
2015-11-20Univs: fix type_of_global_in_context not returning instantiated universe cont...Matthieu Sozeau
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-30Add a way to get the right fix_exn in external vernacular commandsMatthieu Sozeau
2015-10-30More uniformity in the style of comparison functions.Arnaud Spiwack
2015-10-29Make the code of compare functions linear in the number of constructors.Arnaud Spiwack
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-28lib_stack: API to reorder the libstackEnrico Tassi
2015-10-27Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 01:59:00 +0000