aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic
AgeCommit message (Expand)Author
2012-05-15Intuition: temporary(?) restore the unconditional unfolding of notletouzey
2012-04-23remove undocumented and scarcely-used tactic auto decompletouzey
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-11-03Cleaning a little bit the files talking about descriptions: avoidingherbelin
2011-10-05Removing vernacular code mistakenly committed.herbelin
2011-08-23Use of the standard terminology for Diaconescu's theorem (not "paradox").herbelin
2011-08-10Less ambitious application of a notation for eq_rect. We proposedherbelin
2011-08-08New proposition "rewrite Heq in H" for eq_rect (assuming that there isherbelin
2011-07-16Some facts about functional extensionality (especially alternativeherbelin
2011-07-16More lemmas relating the different equivalent formulations of eq_dep.herbelin
2010-12-10First release of Vector library.pboutill
2010-10-23Used multiple lists of implicit arguments to transfer the choices ofherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Made notations for exists, exists! and notations of Utf8.v recursive notationsherbelin
2010-07-22Backported r13308 (ConstructiveEpsilon.v) to branch v8.3herbelin
2010-07-22Update of ConstructiveEpsilon.v by Jean-François Monin.herbelin
2010-06-09Tentative fix for bug #2226: put inj_pair2 and eq_dep_eq hints in amsozeau
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
2010-05-28Generalized the formulation of classic_set in propositional contextsherbelin
2010-05-22Added UIP_dec on suggestion of Eelis on #coq irc.herbelin
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-03-30Small improvements around coqdoc (including fix for bug #2288)herbelin
2009-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...letouzey
2009-11-24Small extra result on JMeq vs eq_dep.herbelin
2009-11-16Some lemmas about dependent choice + extensions of Compare_dec +herbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-27Add a new vernacular command for controling implicit generalization ofmsozeau
2009-10-13MSets: a new generation of FSetsletouzey
2009-09-28Fix the stdlib doc compilation + switch all .v file to utf8letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-03Added "etransitivity".herbelin
2009-05-27Stop using a "Manual Implicit Arguments" flag and support them as soonmsozeau
2009-04-28Backporting 12112 from v8.2 branch to trunk (fixing documentation bugsherbelin
2009-01-27- Fixed various Overfull in documentation.herbelin
2008-12-28- Another bug in get_sort_family_of (sort-polymorphism of constants andherbelin
2008-12-26- Optimized "auto decomp" which had a (presumably) exponential inherbelin
2008-12-17FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...letouzey
2008-12-16Move FunctionalExtensionality to Logic/ (someone please check that themsozeau
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2008-07-15Autour du parsing:herbelin
2008-06-10- Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.herbelin
2008-04-04A file that can be loaded when a migration from Set to Type is desiredletouzey
2008-04-04Correction problème de compil (blast.ml)herbelin
2008-03-30Modifications diverses et variées :herbelin
2008-03-23Nettoyage Wf.v et unification (suite remarques faites sur cocorico)herbelin
2008-03-23Une passe sur les réels:herbelin
2008-03-04migration from Set to Type of FSet/FMap + some dependencies...letouzey
2008-02-02factorization part II (Properties + EqProperties), inclusion of FSetDecide (f...letouzey
2008-01-23Changing R to a local definition so that it isn't exported.roconnor
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-11 05:26:39 +0000