aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Fix new instances that could easily make class resolution loop on Gravatar msozeau2009-10-22
* MSetInterface: some explicit types to avoid Raw.t-instead-of-t effectGravatar letouzey2009-10-21
* FSetCompat: a compatibility wrapper between FSets and MSetsGravatar letouzey2009-10-20
* Merge SetoidList2 into SetoidList: forgotten reference to the removed fileGravatar letouzey2009-10-19
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
* OrderedType2 : trivial lemmas are turned into tests for order.Gravatar letouzey2009-10-16
* Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...Gravatar letouzey2009-10-16
* MSetInterface: (W)Raw2Sets splitted in 2 (helps a future commit by Elie)Gravatar letouzey2009-10-15
* OrderedType2.order is slightly weaker since last commit, adapt accordinglyGravatar letouzey2009-10-15
* OrderedType2.order : fix the last fix (a fail at the wrong place)Gravatar letouzey2009-10-15
* Typo in last commitGravatar letouzey2009-10-14
* Improved tactic "order" in OrderedTypeGravatar letouzey2009-10-14
* Made implicit arguments of Operators_Properties.v localGravatar herbelin2009-10-13
* MSets: a new generation of FSetsGravatar letouzey2009-10-13
* Fix a typo(?) in previous commitGravatar letouzey2009-10-09
* Fixed clash names in Relations (see bug report #2152) and make namesGravatar herbelin2009-10-08
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Implicit argument of Logic.eq become maximally insertedGravatar letouzey2009-10-08
* Correctly do backtracking during type class resolution even if only newGravatar msozeau2009-10-05
* Removal of trailing spaces.Gravatar serpyc2009-10-04
* Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358.Gravatar herbelin2009-10-04
* A few additions in Min.v.Gravatar herbelin2009-10-03
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Add a few properties about Rmin/Rmax with replication in Zmin/Zmax.Gravatar herbelin2009-09-27
* Remove useless MonoList.vGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fix compilation errors due to last commit.Gravatar msozeau2009-09-15
* Stop using [obligation_tactic] from Program.Tactics as the defaultGravatar msozeau2009-09-15
* Added the following lemmas to homogenize Reals a bit:Gravatar gmelquio2009-09-11
* - Resolve type class constraints before trying to find unresolvedGravatar msozeau2009-09-11
* Misc fixes:Gravatar msozeau2009-09-10
* Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsGravatar letouzey2009-09-09
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* Remove unnecessary redefinitions of [Fix_sub] and [Fix_F_sub], asGravatar msozeau2009-09-03
* Fix notation for ~x in theories/Unicode/Utf8.vGravatar glondu2009-08-31
* New tactic to rewrite decidability lemmas when one knows which sideGravatar herbelin2009-08-24
* adds a property on mapGravatar bertot2009-08-19
* adds lemmas on interactions between existsb, forallb, and appGravatar bertot2009-08-19
* Fixed extra space in printing notation { x & P } + minor other thingsGravatar herbelin2009-08-11
* changed deprecated setoid into relationGravatar amahboub2009-08-05
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
* Added "etransitivity".Gravatar herbelin2009-08-03
* OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArithGravatar letouzey2009-07-24
* List: add a iff-based lemma about In and ++Gravatar letouzey2009-07-24
* Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"Gravatar letouzey2009-07-24
* Better comparison functions in OrderedTypeExGravatar letouzey2009-07-22
* Use unfold directly in unfold_equations. Fixes test-suite.Gravatar msozeau2009-07-20
* Typo in a commentGravatar letouzey2009-07-20
* Simplify eauto and fix it for compatibility, allowing full delta duringGravatar msozeau2009-07-14
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 18:08:32 +0000