index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2009-10-28
Same as commit 12430 but with the good version of the function iter_all_segment
soubiran
2009-10-28
From now SearchAbout requests search also inside INCLUDE libobject.
soubiran
2009-10-28
Module type expressions of the form (Fsig X) with Definition foo := bar are n...
soubiran
2009-10-27
Add a new vernacular command for controling implicit generalization of
msozeau
2009-10-27
Fixes around typeclasses:
msozeau
2009-10-27
Added option --external to coqdoc to bind an url to an external library.
herbelin
2009-10-27
Documentation of the Local and Global modifiers.
herbelin
2009-10-27
fix previous commit
corbinea
2009-10-27
fixed czar bug with parametric inductives
corbinea
2009-10-26
Fix Setoid documentation.
msozeau
2009-10-26
Local/Global revision 12418 continued
herbelin
2009-10-26
Adapted test unfold.v after eq gets its argument maximally inserted
herbelin
2009-10-26
New cleaning phase of the Local/Global option management
herbelin
2009-10-26
New functors for gmap and gset.
soubiran
2009-10-25
Restore (and test) broken chaining of lemmas in "apply in" in presence
herbelin
2009-10-25
fixed bug in Czar grammar
corbinea
2009-10-25
Add support for remaining side-conditions in "apply in as".
herbelin
2009-10-25
Improved the treatment of Local/Global options (noneffective Local on
herbelin
2009-10-24
Fixing XML doc (COQ_XML not working as an environment variable).
herbelin
2009-10-23
First debug... the renaming of librairies was not working and auto/dn were no...
soubiran
2009-10-22
Fix new instances that could easily make class resolution loop on
msozeau
2009-10-21
This big commit addresses two problems:
soubiran
2009-10-21
MSetInterface: some explicit types to avoid Raw.t-instead-of-t effect
letouzey
2009-10-20
Repaired bug #2165 (buggy coq example in Tactic Examples doc chapter)
herbelin
2009-10-20
Added syntactic coloration for 'Function'.
gmelquio
2009-10-20
FSetCompat: a compatibility wrapper between FSets and MSets
letouzey
2009-10-19
Merge SetoidList2 into SetoidList: forgotten reference to the removed file
letouzey
2009-10-19
Merge SetoidList2 into SetoidList.
letouzey
2009-10-17
Fixed a notation bug when extending binder_constr with empty levels
herbelin
2009-10-16
OrderedType2 : trivial lemmas are turned into tests for order.
letouzey
2009-10-16
Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...
letouzey
2009-10-16
note for later : when the tag table is shared, never, ever create two
vgross
2009-10-15
typo in doc of Extraction Blacklist
letouzey
2009-10-15
MSetInterface: (W)Raw2Sets splitted in 2 (helps a future commit by Elie)
letouzey
2009-10-15
OrderedType2.order is slightly weaker since last commit, adapt accordingly
letouzey
2009-10-15
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-14
Typo in last commit
letouzey
2009-10-14
Improved tactic "order" in OrderedType
letouzey
2009-10-13
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-09
Fix bug #2162 and a name clashing bug in generalized binders.
msozeau
2009-10-09
Fix a typo(?) in previous commit
letouzey
2009-10-08
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-07
Fix for missing hypotesae in XML proof tree export.
cek
[prev]
[next]