aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2009-10-28Same as commit 12430 but with the good version of the function iter_all_segmentsoubiran
2009-10-28From now SearchAbout requests search also inside INCLUDE libobject.soubiran
2009-10-28Module type expressions of the form (Fsig X) with Definition foo := bar are n...soubiran
2009-10-27Add a new vernacular command for controling implicit generalization ofmsozeau
2009-10-27Fixes around typeclasses:msozeau
2009-10-27Added option --external to coqdoc to bind an url to an external library.herbelin
2009-10-27Documentation of the Local and Global modifiers.herbelin
2009-10-27fix previous commitcorbinea
2009-10-27fixed czar bug with parametric inductivescorbinea
2009-10-26Fix Setoid documentation.msozeau
2009-10-26Local/Global revision 12418 continuedherbelin
2009-10-26Adapted test unfold.v after eq gets its argument maximally insertedherbelin
2009-10-26New cleaning phase of the Local/Global option managementherbelin
2009-10-26New functors for gmap and gset.soubiran
2009-10-25Restore (and test) broken chaining of lemmas in "apply in" in presenceherbelin
2009-10-25fixed bug in Czar grammarcorbinea
2009-10-25Add support for remaining side-conditions in "apply in as".herbelin
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-10-24Fixing XML doc (COQ_XML not working as an environment variable).herbelin
2009-10-23First debug... the renaming of librairies was not working and auto/dn were no...soubiran
2009-10-22Fix new instances that could easily make class resolution loop on msozeau
2009-10-21This big commit addresses two problems:soubiran
2009-10-21MSetInterface: some explicit types to avoid Raw.t-instead-of-t effectletouzey
2009-10-20Repaired bug #2165 (buggy coq example in Tactic Examples doc chapter)herbelin
2009-10-20Added syntactic coloration for 'Function'.gmelquio
2009-10-20FSetCompat: a compatibility wrapper between FSets and MSetsletouzey
2009-10-19Merge SetoidList2 into SetoidList: forgotten reference to the removed fileletouzey
2009-10-19Merge SetoidList2 into SetoidList.letouzey
2009-10-17Fixed a notation bug when extending binder_constr with empty levelsherbelin
2009-10-16OrderedType2 : trivial lemmas are turned into tests for order.letouzey
2009-10-16Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...letouzey
2009-10-16note for later : when the tag table is shared, never, ever create twovgross
2009-10-15typo in doc of Extraction Blacklistletouzey
2009-10-15MSetInterface: (W)Raw2Sets splitted in 2 (helps a future commit by Elie)letouzey
2009-10-15OrderedType2.order is slightly weaker since last commit, adapt accordinglyletouzey
2009-10-15OrderedType2.order : fix the last fix (a fail at the wrong place)letouzey
2009-10-15Fix bug in typeclass resolution discoverd by Eeelis van der Weegen:msozeau
2009-10-14Typo in last commitletouzey
2009-10-14Improved tactic "order" in OrderedTypeletouzey
2009-10-13Made implicit arguments of Operators_Properties.v localherbelin
2009-10-13Typos.gmelquio
2009-10-13Better handling of emphasis.msozeau
2009-10-13MSets: a new generation of FSetsletouzey
2009-10-09Fix bug #2162 and a name clashing bug in generalized binders.msozeau
2009-10-09Fix a typo(?) in previous commitletouzey
2009-10-08Fixed clash names in Relations (see bug report #2152) and make namesherbelin
2009-10-08Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'letouzey
2009-10-08Implicit argument of Logic.eq become maximally insertedletouzey
2009-10-08Fixed a bug introduced in revision 12265.herbelin
2009-10-07Fix for missing hypotesae in XML proof tree export.cek