aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-02-14Do not use global variables for VM bytecode compilation in Cemitcodes.Pierre-Marie Pédrot
2018-02-14Remove the unsafe bytes conversion function in Cemitcodes.Pierre-Marie Pédrot
2018-02-14Move the call to the computation of bytecode inside Cemitcodes.Pierre-Marie Pédrot
2018-02-14Abstract further the type of VM bytecode compilation.Pierre-Marie Pédrot
2018-02-14Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)Maxime Dénès
2018-02-14Merge PR #6713: Fix #6677: Critical bug with VM and universesMaxime Dénès
2018-02-13Add CHANGES entry for #1047Tej Chajed
2018-02-13Merge PR #6693: [toplevel] Refactor command line argument handling.Maxime Dénès
2018-02-13Merge PR #6702: [vernac] [minor] Move print effects to top-level caller.Maxime Dénès
2018-02-13Merge PR #6711: [toplevel] Disable error resiliency in `-quick` mode.Maxime Dénès
2018-02-13Merge PR #6704: Fix coq_makefile not passing -R options to coqdoc, breaking l...Maxime Dénès
2018-02-13Merge PR #6738: CHANGES for universe varianceMaxime Dénès
2018-02-12Merge PR #6565: [Backport script] Check .mli files are not changed.Maxime Dénès
2018-02-12Merge PR #1082: Fixing Print for inductive types with let-in in parametersMaxime Dénès
2018-02-12CHANGES for universe varianceGaëtan Gilbert
2018-02-12Add test case for #6677.Maxime Dénès
2018-02-12Merge PR #6262: [error] Replace msg_error by a proper exception.Maxime Dénès
2018-02-12Merge PR #1047: Support universe instances on the literal TypeMaxime Dénès
2018-02-12Merge PR #6128: Simplification: cumulativity information is variance informa...Maxime Dénès
2018-02-12Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception.Maxime Dénès
2018-02-12Merge PR #6418: More detailed error messages for Canonical Structure, #6398Maxime Dénès
2018-02-12Merge PR #6139: Make list functions returning sumbools transparentMaxime Dénès
2018-02-12Merge PR #6718: Fix redirection to stderr in lint-repository error message.Maxime Dénès
2018-02-12Merge PR #6708: Mention -quiet flag for FailMaxime Dénès
2018-02-12Merge PR #6706: ci-common: guess CI_BRANCH for local buildsMaxime Dénès
2018-02-12Merge PR #6651: Use r.(p) syntax to print primitive projections.Maxime Dénès
2018-02-12Merge PR #6674: Delay computation of lifts in the reduction machine.Maxime Dénès
2018-02-12Fix #6677: Critical bug with VM and universesMaxime Dénès
2018-02-11inferCumulativity: add comment to explain [if not is_arity].Gaëtan Gilbert
2018-02-11Documentation for cumulative inductive variance.Gaëtan Gilbert
2018-02-11Print inductive cumulativity info in About.Gaëtan Gilbert
2018-02-11Universe instance printer: add optional variance argument.Gaëtan Gilbert
2018-02-11Use specialized function for inductive subtyping inference.Gaëtan Gilbert
2018-02-10Inference of inductive subtyping does not need an evar map.Gaëtan Gilbert
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
2018-02-10[get_cumulativity_constraints] allowing further code sharing.Gaëtan Gilbert
2018-02-10Factorize code for comparing maybe-cumulative inductives.Gaëtan Gilbert
2018-02-10Fix typo in Univ.CumulativityInfoGaëtan Gilbert
2018-02-09[vernac] Fix outdated comment.Emilio Jesus Gallego Arias
2018-02-09[nit] Remove some unnecessary global `open Feedback`Emilio Jesus Gallego Arias
2018-02-09[vernac] [minor] Move print effects to top-level caller.Emilio Jesus Gallego Arias
2018-02-09[error] Replace msg_error by a proper exception.Emilio Jesus Gallego Arias
2018-02-09[nativecomp] Remove ad-hoc handling of Dynlink exception.Emilio Jesus Gallego Arias
2018-02-09[toplevel] Small refactoring of fatal_error functions.Emilio Jesus Gallego Arias
2018-02-09[toplevel] Refactor command line argument handling.Emilio Jesus Gallego Arias
2018-02-08Fix redirection to stderr in lint-repository error message.Gaëtan Gilbert
2018-02-07mention interactive mode for Fail messagePaul Steckler
2018-02-07[toplevel] Disable error resiliency in `-quick` mode.Emilio Jesus Gallego Arias
2018-02-07Merge PR #6657: Document the Fail commandMaxime Dénès
2018-02-07Merge PR #6685: Use whd-all on rigid-flex conversion.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 11:09:40 +0000