aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
* Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsGravatar letouzey2009-11-16
* Some lemmas about dependent choice + extensions of Compare_dec +Gravatar herbelin2009-11-16
* Document Generalizable Variables, and change syntax to Gravatar msozeau2009-11-15
* Fix [Instance: forall ..., C args := t] declarations to behave asGravatar msozeau2009-11-15
* BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)Gravatar letouzey2009-11-12
* Repair interpretation of numeral for BigQ, add a printer (close #2160)Gravatar letouzey2009-11-12
* Better compatibility for PeqbGravatar letouzey2009-11-11
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMaxGravatar letouzey2009-11-10
* Simplification of Numbers, mainly thanks to IncludeGravatar letouzey2009-11-10
* DecidableType: A specification via boolean equality as an alternative to eq_decGravatar letouzey2009-11-10
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Use generalizable variables info when internalizing arbitrary bindings,Gravatar msozeau2009-11-08
* Datatypes.length and app defined back via fun+fix instead of FixpointGravatar letouzey2009-11-06
* Numbers: finish files NStrongRec and NDefOpsGravatar letouzey2009-11-06
* Numbers: more (syntactic) changes toward new style of type classesGravatar letouzey2009-11-06
* Numbers: start using Classes stuff, Equivalence, Proper, Instance, etcGravatar letouzey2009-11-03
* ROrderedType + Rminmax : Coq's Reals can be seen as OrderedType.Gravatar letouzey2009-11-03
* Better visibility of the inductive CompSpec used to specify comparison functionsGravatar letouzey2009-11-03
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
* List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...Gravatar letouzey2009-11-02
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
* Added alternate versions of existing lemmas on sqrt.Gravatar gmelquio2009-11-02
* Sorting/Permutation: no need to require the whole Arith (and hence plugins li...Gravatar letouzey2009-11-02
* Operators_Properties: avoid to depend on SetoidGravatar letouzey2009-11-02
* list, length, app are migrated from List to DatatypesGravatar letouzey2009-11-02
* Fix flat_map definition so that it plays nicely with fixGravatar glondu2009-10-29
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 08:26:32 +0000