aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-02-16apply_type: add option "typecheck" passed down to refineEnrico Tassi
2018-02-15Merge PR #1073: new quick2vo target: like vio2vo, but smarterMaxime Dénès
2018-02-15disable tests: vio2vo is broken in WindowsRalf Jung
2018-02-15also test vio2voRalf Jung
2018-02-15test "make quick2vo"Ralf Jung
2018-02-15new quick2vo target: like vio2vo, but smarterRalf Jung
2018-02-15Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProjectMaxime Dénès
2018-02-15coq_makefile: Support "" as the prefix in _CoqProjectJoachim Breitner
2018-02-15Merge PR #6760: CHANGES for 8.7.2.Maxime Dénès
2018-02-14CHANGES for 8.7.2.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 16:04:34 +0000