index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Tentatively trying to restore the use of second-order typed-based
Hugo Herbelin
2015-01-03
*
Fixing #3895 (thanks to PMP for diagnosis).
Hugo Herbelin
2015-01-03
*
An optimization in the use of unification candidates so as to get the
Hugo Herbelin
2015-01-01
*
Document the new behavior of lazymatch.
Guillaume Melquiond
2014-12-30
*
Fixing #3892: Ensure that notation variables do not capture names
Hugo Herbelin
2014-12-30
*
Simplifying second_order_matching: no need to invert the linear
Hugo Herbelin
2014-12-30
*
Compatibility ocaml 3.12.
Hugo Herbelin
2014-12-30
*
more CHANGES
Enrico Tassi
2014-12-30
*
Minor fixes for the win32 installer
Enrico Tassi
2014-12-30
*
Fixing bug #3632 for good.
Pierre-Marie Pédrot
2014-12-29
*
Proof using: do not clear letins (unless they use a cleared var)
Enrico Tassi
2014-12-29
*
Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...
Arnaud Spiwack
2014-12-28
*
Call nf_constraints also when compiling directly to vo
Enrico Tassi
2014-12-28
*
Proof using: call "clear" to remove from sight the vars not selected
Enrico Tassi
2014-12-28
*
remove debug prints (leftover)
Enrico Tassi
2014-12-28
*
STM: check with the kernel proof terms on the worker too
Enrico Tassi
2014-12-27
*
STM: fix processing of errors
Enrico Tassi
2014-12-27
*
STM: module Pp is open
Enrico Tassi
2014-12-27
*
proof_global: make it possible to call close_proof in a worker
Enrico Tassi
2014-12-27
*
include test-suite/coqchk in the summary log
Enrico Tassi
2014-12-27
*
universes_of_constant: do a proper set union of body and type univs
Enrico Tassi
2014-12-27
*
Revert "Term: include a function to print terms"
Enrico Tassi
2014-12-27
*
new test for coqchk
Enrico Tassi
2014-12-26
*
coqchk: flush the pp buffer from time to time
Enrico Tassi
2014-12-26
*
STM: do not call process_error twice (Close: 3880)
Enrico Tassi
2014-12-26
*
Call Evd.nf_constraints only on Univ Poly constants
Enrico Tassi
2014-12-26
*
STM: remove dead code
Enrico Tassi
2014-12-26
*
Term: include a function to print terms
Enrico Tassi
2014-12-26
*
Document 6d5b56d971 (forbid Require inside modules).
Maxime Dénès
2014-12-25
*
Forbid Require inside interactive modules and module types.
Maxime Dénès
2014-12-25
*
Inlining Spawn.kill_if in the one place were it was actually used, thus
Pierre-Marie Pédrot
2014-12-25
*
STM: cleanup code for Admitted
Enrico Tassi
2014-12-23
*
Vi2vo: fix handling of univ constraints coming from the body
Enrico Tassi
2014-12-23
*
Minor modification of CHANGE.
Pierre Courtieu
2014-12-23
*
A global [gfail] tactic which works like [fail] except that it fails even if ...
Arnaud Spiwack
2014-12-23
*
Remove compatibility layer from Ltac's [fail].
Arnaud Spiwack
2014-12-23
*
Fix compilation error in some configurations.
Arnaud Spiwack
2014-12-23
*
Dead code in Univ.
Pierre-Marie Pédrot
2014-12-21
*
Win32: fix installer
Enrico Tassi
2014-12-19
*
Install .v and .glob files too
Enrico Tassi
2014-12-19
*
Add a backtracking version of Ltac's [match].
Arnaud Spiwack
2014-12-19
*
When pretyping [uconstr] closures, don't use the local Ltac variable environm...
Arnaud Spiwack
2014-12-19
*
Fixing performance issue of checker validation.
Pierre-Marie Pédrot
2014-12-19
*
Fixing checker representation of values.
Pierre-Marie Pédrot
2014-12-19
*
update md5 sums to make "make check" work
Enrico Tassi
2014-12-19
*
Fix sigsegv in checker
Enrico Tassi
2014-12-19
*
Better doc and a few fixes for Proof using.
Enrico Tassi
2014-12-19
*
Back to the preferred ?n1:=?n2 order of evar-evar unification which got accid...
Hugo Herbelin
2014-12-19
*
Fixing wrong notation level in #3295.
Hugo Herbelin
2014-12-19
*
Adds two lemmas about hderror to the List standard library.
Sébastien Hinderer
2014-12-18
[next]