aboutsummaryrefslogtreecommitdiff
path: root/theories/MSets
AgeCommit message (Expand)Author
2014-05-09Restore implicit arguments of irreflexivity (fixes bug #3305).Matthieu Sozeau
2014-05-06Try a new way of handling template universe levelsMatthieu Sozeau
2014-05-06- Fix arity handling in retyping (de Bruijn bug!)Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-05-02Cbn is happier when ?SetPositive fixpoints have the set as recursive argumentPierre Boutillier
2014-05-02Eta contractions to please cbnPierre Boutillier
2013-07-17"Boolean Equality" and "Case Analysis" are already off by default...letouzey
2012-12-18No more constant named "int" in Coq theories (cf bug #2878)letouzey
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-01Ltac repeat is in fact already doing progressletouzey
2012-08-06MSetRBT: a tail-recursive plengthletouzey
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
2012-07-05MSetRBT : elementary arith proofs instead of calls to lialetouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-04-13MSetRBT : implementation of MSets via Red-Black treesletouzey
2012-01-17MSetAVL: better implementation of filter suggested by X. Leroyletouzey
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-10-14MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_rightletouzey
2011-10-07fsetdec : non-atomic elements are now transformed as variables first (fix #2464)letouzey
2011-10-07Improved handling of element equalities in fsetdec (fix #2467)letouzey
2011-05-05Modularization of BinInt, related fixes in the stdlibletouzey
2011-03-17CompareSpec: a slight generalization/reformulation of CompSpecletouzey
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-02-17- Use transparency information all the way through unification andmsozeau
2011-01-06s/appartness/membership/g (Closes: #2470)glondu
2010-09-20Extraction: re-introduce some eta-expansions in rare situations leading to '_...letouzey
2010-09-17For the moment, two small manual eta-expansions to avoid '_a after extractionletouzey
2010-07-22Made notations for exists, exists! and notations of Utf8.v recursive notationsherbelin
2010-07-16MSetPositive: mention MSetInterface instead of FSetInterfaceletouzey
2010-07-16FSetPositive: sets of positive inspired by FMapPositive.letouzey
2010-07-05FSets/Msets: some renaming of module params to simplify the task of the extra...letouzey
2010-06-18Report fixes from FSetDecide to MSetDecideletouzey
2010-06-16MSetInterface: no induction principle about a Record (nicer extraction)letouzey
2010-06-15MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and tre...letouzey
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-09Change definition of FSetList so that equality is Leibnizglondu
2010-02-12CompSpecType, a clone of CompSpec but in Type instead of Propletouzey
2010-01-12MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)letouzey
2010-01-07Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*letouzey
2010-01-07Include can accept both Module and Module Typeletouzey
2010-01-07MSetInterface: more modularityletouzey
2010-01-07MSetAVL: hints made local since some of them are quite violent (transitivity)letouzey
2010-01-05Avoid declaring hints about refl/sym/trans of eq in DecidableType2letouzey
2010-01-04Specific syntax for Instances in Module Type: Declare Instanceletouzey
2009-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...letouzey
2009-12-08integrate MSetToFiniteSet into the compilation (and fix it)letouzey
2009-11-30Fix backtracking heuristic in typeclass resolution. msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-12 18:11:37 +0000