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
*
OrderedType2.order : fix the last fix (a fail at the wrong place)
letouzey
2009-10-15
*
Fix bug in typeclass resolution discoverd by Eeelis van der Weegen:
msozeau
2009-10-15
*
Typo in last commit
letouzey
2009-10-14
*
Improved tactic "order" in OrderedType
letouzey
2009-10-14
*
Made implicit arguments of Operators_Properties.v local
herbelin
2009-10-13
*
Typos.
gmelquio
2009-10-13
*
Better handling of emphasis.
msozeau
2009-10-13
*
MSets: a new generation of FSets
letouzey
2009-10-13
*
Fix bug #2162 and a name clashing bug in generalized binders.
msozeau
2009-10-09
*
Fix a typo(?) in previous commit
letouzey
2009-10-09
*
Fixed clash names in Relations (see bug report #2152) and make names
herbelin
2009-10-08
*
Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'
letouzey
2009-10-08
*
Implicit argument of Logic.eq become maximally inserted
letouzey
2009-10-08
*
Fixed a bug introduced in revision 12265.
herbelin
2009-10-08
*
Fix for missing hypotesae in XML proof tree export.
cek
2009-10-07
*
Fixed installation of Coqide interface/library files (bug #2147).
gmelquio
2009-10-06
*
Relaxed error severity when encountering unknown library objects or tactic
gmelquio
2009-10-06
*
Correctly do backtracking during type class resolution even if only new
msozeau
2009-10-05
*
Revert "kills the old backtracking framework and replaces it with"
vgross
2009-10-05
*
Changed the way to support compatibility with previous versions.
herbelin
2009-10-04
*
Removal of trailing spaces.
serpyc
2009-10-04
*
Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358.
herbelin
2009-10-04
*
Fixed small name freshness bug in Functional Scheme ("Heq" name was
herbelin
2009-10-03
*
A few additions in Min.v.
herbelin
2009-10-03
*
Added option "Unset Dependent Propositions Elimination" to protect
herbelin
2009-10-03
*
Add support for Local Declare ML Module
glondu
2009-09-29
*
Remove legacy export_* functions
glondu
2009-09-29
*
kills the old backtracking framework and replaces it with
vgross
2009-09-29
*
Fix the stdlib doc compilation + switch all .v file to utf8
letouzey
2009-09-28
*
Applied patches from BSD/pkgsrc maintainer, so that Coq compiles out-of-the-box.
gmelquio
2009-09-28
*
Apply "Declare Implicit Tactic" also to terms interpreted as "open
herbelin
2009-09-27
*
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
*
Add a few properties about Rmin/Rmax with replication in Zmin/Zmax.
herbelin
2009-09-27
*
Fixed error message "cannot infer the type of id" in presence of
herbelin
2009-09-27
*
Delay the choice of eliminator in destruct/induction until we know if
herbelin
2009-09-27
*
Complement to 12347 and 12348 on the extended syntax of case/elim.
herbelin
2009-09-27
*
Fixed a hole in glob_tactic that allowed some Ltac code to refer to
herbelin
2009-09-26
*
Micromega doc : psatz Z -> psatz Z 2
fbesson
2009-09-24
*
Ltac doc: only variables are accepted as message_token
glondu
2009-09-23
*
Add the option to automatically introduce variables declared before the
msozeau
2009-09-22
*
Better use of transparency information for local hypotheses:
msozeau
2009-09-22
*
Update link to "Recursive Make Considered Harmful"
glondu
2009-09-21
*
Only one "in" clause in "destruct" even for a multiple "destruct".
herbelin
2009-09-20
*
Add "case as/in/using" and temporary "destruct" with n args.
herbelin
2009-09-20
*
micromega: better handling of exponentiation + correction of test-suite termi...
fbesson
2009-09-18
*
- Fixed a bug in checking that implicit arguments are all correctly
herbelin
2009-09-18
*
Replace call to where_in_path by find_file_in_path in "Locate File"
glondu
2009-09-17
*
Replace unprotected call to where_in_path by find_file_in_path
glondu
2009-09-17
*
Remove useless MonoList.v
glondu
2009-09-17
[next]