index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
Commit message (
Expand
)
Author
Age
*
Fixed a notation bug when extending binder_constr with empty levels
herbelin
2009-10-17
*
Fixed a bug introduced in revision 12265.
herbelin
2009-10-08
*
Removal of trailing spaces.
serpyc
2009-10-04
*
Fixed a bug in the interaction between dEqThen and inject_at_positions
herbelin
2009-09-27
*
Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.
herbelin
2009-09-27
*
Delay the choice of eliminator in destruct/induction until we know if
herbelin
2009-09-27
*
Micromega doc : psatz Z -> psatz Z 2
fbesson
2009-09-24
*
Add the option to automatically introduce variables declared before the
msozeau
2009-09-22
*
Only one "in" clause in "destruct" even for a multiple "destruct".
herbelin
2009-09-20
*
micromega: better handling of exponentiation + correction of test-suite termi...
fbesson
2009-09-18
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0...
fbesson
2009-08-25
*
+ csdp.cache
fbesson
2009-08-15
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
Ensures that let-in's in arities of inductive types work well. Maybe not
herbelin
2009-08-11
*
Relatively ad hoc fix to an ill-typed instantiation bug in type
herbelin
2009-08-11
*
psatz Z -> psatz Z 1
fbesson
2009-07-30
*
Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"
letouzey
2009-07-24
*
Move some examples for groebner into a test-suite file
letouzey
2009-07-20
*
- Granted wish #2138 (support for local binders in syntax of Record fields).
herbelin
2009-07-15
*
Reactivation of pattern unification of evars in apply unification, in
herbelin
2009-07-08
*
Fixing bug #2106 ("match" compilation with multi-dependent constructor).
herbelin
2009-06-06
*
Adding a regression test about Bauer's example on coq-club of
herbelin
2009-06-02
*
Fix script file using the "Manual Implicit" flag.
msozeau
2009-06-02
*
micromega: proof compression bugfix
fbesson
2009-05-11
*
- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it
herbelin
2009-05-10
*
- Fixing #2090 (occur check missing when trying to solve evar-evar equation).
herbelin
2009-04-25
*
Fix test output mentionning an existential number that changed.
msozeau
2009-04-20
*
Fix wrong pattern in Morphisms. Fix bug scripts to reflect the fact that
msozeau
2009-04-20
*
Fix bug #2089: correctly dealing with parameters and real arguments in
msozeau
2009-04-16
*
Fix and actually beautify the bug script to adapt to the new measure
msozeau
2009-04-14
*
Fix premature optimisation in dependent induction: even variable args need
msozeau
2009-04-10
*
- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing
herbelin
2009-04-08
*
Add tests for quote
glondu
2009-03-30
*
Avoid inadvertent declaration of "on" as a keyword. New syntax is
msozeau
2009-03-29
*
Rewrite of Program Fixpoint to overcome the previous limitations:
msozeau
2009-03-28
*
Fixes in Program well-founded definitions:
msozeau
2009-03-26
*
coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...
barras
2009-03-19
*
Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"
herbelin
2009-03-16
*
illegal tactic application was having Ltac interpreter loop
barras
2009-03-04
*
Add support for dependent "destruct" over terms in dependent types.
herbelin
2009-02-23
*
commited complexity test for exponential behavior of unification
barras
2009-02-09
*
Fixing #2044 (bad printing of primitive notation at the head of
herbelin
2009-02-06
*
From v8.2 to trunk:
herbelin
2009-02-06
*
Report r11631 from 8.2 and handle non-dependent goals better in
msozeau
2009-02-04
*
Fixes in the documentation of [dependent induction] and test-suite
msozeau
2009-01-22
*
Fixing bug #1918 (no occur-check in Meta unification was done yet!).
herbelin
2009-01-20
*
- Fixing bug 1891 (abusive instantiations of evar arguments in
herbelin
2009-01-20
*
The initial state evar numbering increased. Fix output message in a test.
puech
2009-01-19
*
Backporting from v8.2 to trunk:
herbelin
2009-01-18
[next]