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
*
moins de reification inutile, noatations standards
pottier
2011-08-04
*
Relaxed the constraint introduced in r14190 that froze the existing
herbelin
2011-06-18
*
add names of theorems in output
jnarboux
2011-06-18
*
Tests de nsatz avec la geometrie
pottier
2011-06-16
*
Added full pattern-unification on Meta for tactic unification.
herbelin
2011-06-13
*
Another bug of Scheme Induction (generated names dep/nodep were swapped).
herbelin
2011-06-13
*
Fixing an anomaly in Scheme Induction.
herbelin
2011-06-13
*
Added a new flag for freezing evars in tactic unification. Used this
herbelin
2011-06-12
*
Fixing another bug with "_" intro pattern.
herbelin
2011-06-10
*
Made use of "_" in repeated use of intros_patterns work (with
herbelin
2011-06-10
*
ring2, cring, nsatz avec type classe avec parametres plus notations
pottier
2011-06-10
*
Mini-test for eta
herbelin
2011-05-26
*
Partial fix for accepting bound variables with same name as implicit
herbelin
2011-05-26
*
Fixing discriminate for identity.
herbelin
2011-05-26
*
Add simple test of bullet behaviour.
aspiwack
2011-05-17
*
Fixes in the test-suite after modularisation of ZArith and co
letouzey
2011-05-06
*
Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixed
herbelin
2011-04-28
*
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
*
Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)
letouzey
2011-03-16
*
Fix inductive_template building ill-typed evars, and update test-suite scripts
msozeau
2011-03-13
*
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
*
Correct handling of existential variables when multiple different
msozeau
2011-02-08
*
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
*
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
*
test-suite: fix success/unification.v
glondu
2010-10-07
*
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
*
Fixing bugs in previous commits about implicit arguments:
herbelin
2010-10-04
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Improve handling of metas as evars in unification (patch by Hugo)
letouzey
2010-09-30
*
Fixed a problem introduced in r12607 after pattern_of_constr served
herbelin
2010-09-17
*
In the computation of missing arguments for apply, accept that the
herbelin
2010-09-17
*
Improving a few error messages in Ltac interpretation
herbelin
2010-09-11
*
unification des tactiques nsatz pour R Z avec celle des anneaux integres
pottier
2010-07-28
*
nstaz pour les anneaux integres et les setoides, R Z et Q
pottier
2010-07-27
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
[next]