index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit 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-08
Fix redirection to stderr in lint-repository error message.
Gaëtan Gilbert
2018-02-08
pre-commit: nicer messages
Gaëtan Gilbert
2018-02-08
pre-commit: fail gracefully if fixing whitespace removes all changes
Gaëtan Gilbert
2018-02-08
pre-commit: add files after fixing ending newlines.
Gaëtan Gilbert
2018-02-08
Document configure setting up pre-commit hook in CONTRIBUTING.md
Gaëtan Gilbert
2018-02-08
Have the pre-commit hook also fix end-of-file nl
Jason Gross
2018-02-08
Auto-create .git/hooks/pre-commit on ./configure
Jason Gross
2018-02-08
pre-commit hook: fix whitespace error detection
Gaëtan Gilbert
2018-02-08
Mention linter and pre-commit hook in CONTRIBUTING.md.
Gaëtan Gilbert
2018-02-08
A pre-commit hook to magically fix whitespace issues.
Gaëtan Gilbert
2018-02-07
mention interactive mode for Fail message
Paul Steckler
2018-02-07
[toplevel] Disable error resiliency in `-quick` mode.
Emilio Jesus Gallego Arias
2018-02-07
Merge PR #6657: Document the Fail command
Maxime Dénès
2018-02-07
Merge PR #6685: Use whd-all on rigid-flex conversion.
Maxime Dénès
2018-02-07
Merge PR #6610: Points to Flocq official repository.
Maxime Dénès
2018-02-07
Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding
Maxime Dénès
2018-02-07
Merge PR #6673: Fix evar handling in native_compute conversion
Maxime Dénès
2018-02-07
ci-common: guess CI_BRANCH for local builds
Gaëtan Gilbert
2018-02-07
Possible fix for issue #6697
Yannick Forster
2018-02-06
More detailed error messages for Canonical Structure, #6398
Paul Steckler
2018-02-06
Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.
Maxime Dénès
2018-02-06
Merge PR #6695: [toplevel] Refine start of interactive mode conditions.
Maxime Dénès
2018-02-05
Points to Flocq official repository.
Théo Zimmermann
2018-02-05
Respect the transparent state of the current conversion on strong weak-head.
Pierre-Marie Pédrot
2018-02-05
Add overlay for equations (nf_beta takes an env)
Gaëtan Gilbert
2018-02-05
[native_compute] Fix handling of evars in conversion
Maxime Dénès
2018-02-05
[native_compute] Remove useless conversion to list in reification.
Maxime Dénès
2018-02-05
Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in Ve...
Maxime Dénès
2018-02-05
Merge PR #6654: CI: Run coqchk on Iris
Maxime Dénès
2018-02-05
Merge PR #6652: Allow vernacular controls before focus selector
Maxime 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-04
Delay computation of lifts in the reduction machine.
Pierre-Marie Pédrot
2018-02-02
CClosure.unfold_projection: don't catch Not_found, assume env is ok
Gaëtan Gilbert
2018-02-02
Reductionops.nf_* now take an environment.
Gaëtan Gilbert
2018-02-02
checker: cleanup projection unfolding
Gaëtan Gilbert
2018-02-02
checker: remove unused per-constant reduction flags.
Gaëtan Gilbert
2018-02-02
kernel: cleanup projection unfolding
Gaëtan Gilbert
2018-02-02
Use whd-all on rigid-flex conversion.
Pierre-Marie Pédrot
2018-02-01
Merge PR #6670: Delete duplicate line
Maxime Dénès
2018-02-01
Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant e...
Maxime Dénès
2018-02-01
Merge PR #6672: [stm] Move options to a per-document record.
Maxime Dénès
2018-02-01
Merge PR #6660: [lib] Respect change of options under with/without_option.
Maxime Dénès
[prev]
[next]