aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FSetDecide.v
Commit message (Expand)AuthorAge
* Forbid Require inside interactive modules and module types.Gravatar Maxime Dénès2014-12-25
* fsetdec : non-atomic elements are now transformed as variables first (fix #2464)Gravatar letouzey2011-10-07
* Improved handling of element equalities in fsetdec (fix #2467)Gravatar letouzey2011-10-07
* fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix #2...Gravatar letouzey2010-06-18
* fsetdec: clear dependent hypothesis before anything else (fix #2136).Gravatar letouzey2010-06-17
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...Gravatar letouzey2008-12-17
* integrate suggestions by B. Baydemir (see #1930)Gravatar letouzey2008-11-17
* avoid duplicated creation of WFacts instancesGravatar letouzey2008-06-06
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
* repair FSets/FMap after the change in setoid rewriteGravatar letouzey2008-03-07
* Reorganization of FSet+FMap : no more files specific to Weak Sets/MapsGravatar letouzey2008-02-04
* factorization part II (Properties + EqProperties), inclusion of FSetDecide (f...Gravatar letouzey2008-02-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 09:05:26 +0000