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
*
Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".
herbelin
2011-04-15
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
- Do not make constants with an assigned type polymorphic (wrong unfoldings).
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v
herbelin
2011-04-08
*
Fixing multiple printing bugs with "Notation f x := ..."
herbelin
2011-04-08
*
Did that adding a rule for printing applications as "f(x)" works.
herbelin
2011-03-31
*
Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)
letouzey
2011-03-16
*
Adapt test-suite/output/Extraction_matchs_2413 to new indentation of extraction
letouzey
2011-03-16
*
Fix inductive_template building ill-typed evars, and update test-suite scripts
msozeau
2011-03-13
*
Starting being more explicit on the reasons why module subtyping fails.
herbelin
2011-03-05
*
Improved define_evar_as_lambda which was creating an unrelated new evar
herbelin
2011-03-05
*
Try to fix the behavior of clenv_missing used when declaring hints
letouzey
2011-02-22
*
Some fixes of the test-suite scripts
letouzey
2011-02-21
*
Fix test-suite script.
msozeau
2011-02-21
*
MacOS compatibility
pboutill
2011-02-10
*
Correct handling of existential variables when multiple different
msozeau
2011-02-08
*
test-suite/Makefile: add a rule to build all_stdlib.v (for the bench)
glondu
2011-01-27
*
Add a test for sorting all universes of stdlib
glondu
2011-01-25
*
Add "Print Sorted Universes"
glondu
2011-01-11
*
Fixing an uncaught exception bug with use of vmcast
herbelin
2011-01-07
*
Remove the two-argument variant of "decide equality"
glondu
2010-12-23
*
Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)
letouzey
2010-12-21
*
Fixing bug #2454: inversion predicate strategy for inferring the type
herbelin
2010-12-19
*
Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).
herbelin
2010-12-04
*
Fixing bug using explictly declared implicit arguments in inductive arities.
herbelin
2010-12-03
*
Fixing a bug introduced in r12304 (move of interpretation of
herbelin
2010-12-02
*
SearchAbout: who has never been annoyed by the [ ] syntax ?
letouzey
2010-11-19
*
An experimental support for open constrs in hints and in "using"
herbelin
2010-10-31
*
Fix missing -coqlib argument to coqdep in test-suite
glondu
2010-10-16
*
Adding test-case for bug #2362, which uses HO unification during
msozeau
2010-10-12
*
Fix bug #2393: allow let-ins inside telescopes (only fails when there's
msozeau
2010-10-12
*
Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, looping
herbelin
2010-10-11
*
test-suite: fix success/unification.v
glondu
2010-10-07
*
test-suite: fix output/Existentials.out
glondu
2010-10-06
*
test-suite: fix success/Typeclasses.v
glondu
2010-10-05
*
test-suite: fix success/AdvancedCanonicalStructure.v
glondu
2010-10-05
*
Export definition of type implicits_list for contribs + fixed a
herbelin
2010-10-05
*
test-suite: use unified diff output and use expected output as reference
glondu
2010-10-05
*
Fixing bugs in previous commits about implicit arguments:
herbelin
2010-10-04
*
Test for non-regression of the display bug fixed in r13486.
herbelin
2010-10-03
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Making display of various informations about constants more modular:
herbelin
2010-10-03
*
Improve handling of metas as evars in unification (patch by Hugo)
letouzey
2010-09-30
*
Fix inconsistency in Prop/Set conversion check
glondu
2010-09-23
*
Fixed test of bug #2360 (use of Fail to check a regular error instead
herbelin
2010-09-20
*
Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't we
herbelin
2010-09-19
*
Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" in
herbelin
2010-09-18
*
Fixing bugs #2347 (part 2) and #2388: error message printing was done
herbelin
2010-09-18
*
Fixed a problem introduced in r12607 after pattern_of_constr served
herbelin
2010-09-17
[next]