index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
success
Commit message (
Expand
)
Author
Age
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-13
|
\
|
*
Fixing #4467 (continued).
Hugo Herbelin
2016-01-13
|
*
Extend last commit: keyed unification uses full conversions on the applied co...
Matthieu Sozeau
2016-01-12
|
*
Extend Keyed Unification tests with the one from R. Krebbers.
Matthieu Sozeau
2016-01-12
*
|
Fixing a bug in the order of side conditions for introduction pattern -> and <-.
Hugo Herbelin
2015-12-25
*
|
Fixing an "injection as" bug in the presence of side conditions.
Hugo Herbelin
2015-12-25
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-17
|
\
|
|
*
Proof using: do not clear unused section hyps automatically
Enrico Tassi
2015-12-15
|
*
Fix test-suite files after change in refine tactic.
Maxime Dénès
2015-12-15
|
*
Adding a test for the unshelve tactical.
Pierre-Marie Pédrot
2015-12-15
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-15
|
\
|
|
*
extraction_impl.v: fix a typo
Pierre Letouzey
2015-12-14
|
*
A test file for Extraction Implicit (including bugs #4243 and #4228)
Pierre Letouzey
2015-12-14
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-11
|
\
|
|
*
Fixing a pat%constr bug. Thanks to Enrico for reporting.
Hugo Herbelin
2015-12-10
|
*
Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.
Hugo Herbelin
2015-12-10
|
*
bug fixes to vm computation + test cases.
Gregory Malecha
2015-12-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
|
|
*
Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)
Hugo Herbelin
2015-12-05
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-03
|
\
|
|
*
Improving syntax of pat/constr introduction pattern so that
Hugo Herbelin
2015-12-02
|
*
Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.
Hugo Herbelin
2015-12-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
|
*
Fixing the "parsing rules with idents later declared as keywords" problem.
Hugo Herbelin
2015-11-26
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-26
|
\
|
|
*
Fixing a vm_compute bug in the presence of let-ins among the
Hugo Herbelin
2015-11-22
|
*
Fixing a bug of adjust_subst_to_rel_context.
Hugo Herbelin
2015-11-22
|
*
Fixing kernel bug in typing match with let-ins in the arity.
Hugo Herbelin
2015-11-22
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
|
\
|
|
*
Fixing logical bugs in the presence of let-ins in computiong primitive
Hugo Herbelin
2015-11-18
*
|
Merge origin/v8.5 into trunk
Hugo Herbelin
2015-11-10
|
\
|
|
*
Tests for syntax "Show id" and [id]:tac (shelved or not).
Hugo Herbelin
2015-11-07
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
*
Hint Cut documentation and cleanup of printing (was duplicated and
Matthieu Sozeau
2015-11-04
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-30
|
\
|
|
*
Handle side-effects of Vernacular commands inside proofs better, so that
Matthieu Sozeau
2015-10-29
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
*
Fix test suite after Matthieu's ed7af646f2e486b.
Maxime Dénès
2015-10-28
|
*
Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"
Hugo Herbelin
2015-10-28
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-19
|
\
|
|
*
Fixing #4198 (continued): not matching within the inner lambdas/let-ins
Hugo Herbelin
2015-10-18
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-12
|
\
|
|
*
Refining 0c320e79ba30 in fixing interpretation of constr under binders
Hugo Herbelin
2015-10-11
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
*
Proof using: let-in policy, optional auto-clear, forward closure*
Enrico Tassi
2015-10-08
|
*
Test for record syntax parsing.
Pierre-Marie Pédrot
2015-10-07
|
*
Univs: add Strict Universe Declaration option (on by default)
Matthieu Sozeau
2015-10-07
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-09-17
|
\
|
[next]