aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-02-15coq_makefile: Support "" as the prefix in _CoqProjectJoachim Breitner
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-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[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-08Fix redirection to stderr in lint-repository error message.Gaëtan Gilbert
2018-02-07mention interactive mode for Fail messagePaul Steckler
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
2018-02-07Merge PR #6610: Points to Flocq official repository.Maxime Dénès
2018-02-07Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingMaxime Dénès
2018-02-07Merge PR #6673: Fix evar handling in native_compute conversionMaxime Dénès
2018-02-07ci-common: guess CI_BRANCH for local buildsGaëtan Gilbert
2018-02-06More detailed error messages for Canonical Structure, #6398Paul Steckler
2018-02-06Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.Maxime Dénès
2018-02-06Merge PR #6695: [toplevel] Refine start of interactive mode conditions.Maxime Dénès
2018-02-05Points to Flocq official repository.Théo Zimmermann
2018-02-05Respect the transparent state of the current conversion on strong weak-head.Pierre-Marie Pédrot
2018-02-05Add overlay for equations (nf_beta takes an env)Gaëtan Gilbert
2018-02-05[native_compute] Fix handling of evars in conversionMaxime Dénès
2018-02-05[native_compute] Remove useless conversion to list in reification.Maxime Dénès
2018-02-05Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in Ve...Maxime Dénès
2018-02-05Merge PR #6654: CI: Run coqchk on IrisMaxime Dénès
2018-02-05Merge PR #6652: Allow vernacular controls before focus selectorMaxime Dénès
2018-02-05[stm] [toplevel] Make loadpath a parameter of the document.Emilio Jesus Gallego Arias
2018-02-05[toplevel] Refine start of interactive mode conditions.Emilio Jesus Gallego Arias
2018-02-04Delay computation of lifts in the reduction machine.Pierre-Marie Pédrot
2018-02-02CClosure.unfold_projection: don't catch Not_found, assume env is okGaëtan Gilbert
2018-02-02Reductionops.nf_* now take an environment.Gaëtan Gilbert
2018-02-02checker: cleanup projection unfoldingGaëtan Gilbert
2018-02-02checker: remove unused per-constant reduction flags.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 04:00:55 +0000