aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-08pre-commit: nicer messagesGaëtan Gilbert
2018-02-08pre-commit: fail gracefully if fixing whitespace removes all changesGaëtan Gilbert
2018-02-08pre-commit: add files after fixing ending newlines.Gaëtan Gilbert
2018-02-08Document configure setting up pre-commit hook in CONTRIBUTING.mdGaëtan Gilbert
2018-02-08Have the pre-commit hook also fix end-of-file nlJason Gross
2018-02-08Auto-create .git/hooks/pre-commit on ./configureJason Gross
2018-02-08pre-commit hook: fix whitespace error detectionGaëtan Gilbert
2018-02-08Mention linter and pre-commit hook in CONTRIBUTING.md.Gaëtan Gilbert
2018-02-08A pre-commit hook to magically fix whitespace issues.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
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-07Possible fix for issue #6697Yannick Forster
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
2018-02-02kernel: cleanup projection unfoldingGaëtan Gilbert
2018-02-02Use whd-all on rigid-flex conversion.Pierre-Marie Pédrot
2018-02-01Merge PR #6670: Delete duplicate lineMaxime Dénès
2018-02-01Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant e...Maxime Dénès
2018-02-01Merge PR #6672: [stm] Move options to a per-document record.Maxime Dénès
2018-02-01Merge PR #6660: [lib] Respect change of options under with/without_option.Maxime Dénès