aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* Fix the build of coq via ocamlbuildGravatar letouzey2009-12-08
* integrate MSetToFiniteSet into the compilation (and fix it)Gravatar letouzey2009-12-08
* No more specific syntax "Include Self" for inclusion of partially-applied fun...Gravatar letouzey2009-12-07
* Forgot a file in last commit.Gravatar msozeau2009-12-06
* Fix anomaly when using typeclass resolution with filtered hyps in evars.Gravatar msozeau2009-12-06
* Rename proper to proper_prf to avoid clash with CoRN, Gravatar msozeau2009-12-03
* Fix make_exact_entry to allow applying [forall x, P x] hints directly,Gravatar msozeau2009-12-01
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Minor fixes in typeclasses, avoiding repeated evar normalizations.Gravatar msozeau2009-11-24
* Small extra result on JMeq vs eq_dep.Gravatar herbelin2009-11-24
* Diamond-shape instead of linear hiearchy in Numbers/NatIntGravatar letouzey2009-11-18
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 03:14:22 +0000