index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2017-09-22
Merge PR #1070: Remove remaining occurrences of -just-parsing.
Maxime Dénès
2017-09-22
Merge PR #1064: coq_makefile: dont show errors from failed (ignored) rmdir
Maxime Dénès
2017-09-22
Merge PR #1063: [flags] Flag `open Flags`
Maxime Dénès
2017-09-22
Merge PR #1061: Fix appveyor build
Maxime Dénès
2017-09-21
Report missing arguments in error message
Tej Chajed
2017-09-21
Properly handle "coq_makefile -Q . Foo" (bug #5580).
Guillaume Melquiond
2017-09-21
Fix -silent flag of coqchk after ff918e4.
Maxime Dénès
2017-09-21
Adapt checker to change in locations.
Maxime Dénès
2017-09-21
Proposing meta names more distinguishable from evar names than ?M42.
Hugo Herbelin
2017-09-21
A possible fix to BZ#5750 (ability to print context of ltac subterm match).
Hugo Herbelin
2017-09-21
[checker] Add missing Feedback printer (BZ#5587)
Emilio Jesus Gallego Arias
2017-09-21
Do not run Travis OS X packaging job on PRs
Théo Zimmermann
2017-09-21
Do not reinstall preinstalled packages under AppVeyor.
Maxime Dénès
2017-09-21
Print Cygwin setup output rather than logging in to a file.
Maxime Dénès
2017-09-21
Mark "Set Tactic Compat Context" as deprecated.
Guillaume Melquiond
2017-09-21
Remove remaining occurrences of -just-parsing.
Guillaume Melquiond
2017-09-21
Improve support for "-w none" compatibility option.
Guillaume Melquiond
2017-09-21
Handle multiple -w options on command line (bug #5736).
Guillaume Melquiond
2017-09-20
In gitlab set TRAVIS_BRANCH so user overlays will work as expected.
Gaëtan Gilbert
2017-09-20
coq_makefile: dont show errors from failed (ignored) rmdir
Ralf Jung
2017-09-20
ssr: fix canonical strucut key comparison with primproj on
Enrico Tassi
2017-09-20
[flags] Flag `open Flags`
Emilio Jesus Gallego Arias
2017-09-19
An optimization of tactic constructor.
Hugo Herbelin
2017-09-19
coq_makefile: make sure compile flags for Coq and coq_makefile are in sync
Emilio Jesus Gallego Arias
2017-09-19
Fixing bug #5741 (anomaly in info_trivial).
Hugo Herbelin
2017-09-19
Merge PR #1036: Unify EConstr.t equality
Maxime Dénès
2017-09-19
Improve documentation of Status message.
Maxime Dénès
2017-09-19
Remove STM vernaculars.
Maxime Dénès
2017-09-19
Add XML protocol support for Wait.
Maxime Dénès
2017-09-19
Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).
Maxime Dénès
2017-09-19
Merge PR #1043: Disable OSX signing for temporary artifacts.
Maxime Dénès
2017-09-19
Document UState.universe_context.
Gaëtan Gilbert
2017-09-19
Don't lose names in UState.universe_context.
Gaëtan Gilbert
2017-09-19
test-suite: polymorphism
Matthieu Sozeau
2017-09-19
proof_global: cleanup and comment close_proof
Matthieu Sozeau
2017-09-19
Allow declaring universe binders with no constraints with @{|}
Gaëtan Gilbert
2017-09-19
Allow declaring universe constraints at definition level.
Matthieu Sozeau
2017-09-19
Allow empty instance parsing @{}
Matthieu Sozeau
2017-09-19
Merge PR #1024: Switch Travis to OSX 10.12 and Xcode 8.3.3.
Maxime Dénès
2017-09-19
Merge PR #920: kernel: bugfix in filter_stack_domain.
Maxime Dénès
2017-09-18
Reporting locations in error messages about notation formats.
Hugo Herbelin
2017-09-18
Fixing two anomalies in corner cases of the syntax of notation formats.
Hugo Herbelin
2017-09-18
Add test-suite script by Cyprien Mangin
Matthieu Sozeau
2017-09-15
Merge PR #979: Fix install-doc target and other gitlab failures
Maxime Dénès
2017-09-15
Fix CHANGES after merge of PR #1025.
Théo Zimmermann
2017-09-15
Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...
Maxime Dénès
2017-09-15
Merge PR #1051: Using an algebraic type for distinguishing toplevel input fro...
Maxime Dénès
2017-09-15
Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.
Maxime Dénès
2017-09-15
Merge PR #1046: Better error messages, fix for BZ#5723
Maxime Dénès
2017-09-15
Merge PR #1045: Remove unneeded fix for BZ#1715
Maxime Dénès
[prev]
[next]