aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Relations/Operators_Properties.v
Commit message (Collapse)AuthorAge
* A couple of fixes/improvements in -beautify, but backtracking onGravatar Hugo Herbelin2014-08-12
| | | | change of printing format of forall (need more thinking).
* Small lemma about Relations.Gravatar Hugo Herbelin2014-06-04
|
* Fixing #3089. This implied tweaking the definition of the lexicographicGravatar ppedrot2013-07-26
| | | | | | | | product of lists, hence possibly introducing incompatibilities. Parts of the patch by Chantal Keller. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16635 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
| | | | | | | Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Operators_Properties: avoid to depend on SetoidGravatar letouzey2009-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12453 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made implicit arguments of Operators_Properties.v localGravatar herbelin2009-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12387 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a typo(?) in previous commitGravatar letouzey2009-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12382 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed clash names in Relations (see bug report #2152) and make namesGravatar herbelin2009-10-08
| | | | | | | | in Relation_Operators.v and Operators_Properties.v more uniform in general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12381 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour en arrière sur la mise en paramètre du premier argument deGravatar herbelin2008-10-19
| | | | | | | | | Coq.Relation.Relation_Operators.clos_refl_sym_trans car cela échange les arguments de rst_sym et casse la compatibilité (cf p.ex. Rocq/PTS). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11471 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration et formattage du développement de Pierre Castéran sur lesGravatar herbelin2008-10-18
| | | | | | | | définitions alternatives de la transitivé d'une relation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11462 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage de Set à Type dans Relations et WellfoundedGravatar herbelin2007-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9598 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en forme des theoriesGravatar notin2006-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵Gravatar herbelin2003-11-29
| | | | | | par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de Induction/Destruct par NewInduction/NewDestructGravatar herbelin2003-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4464 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
* remplace Zarith par ZArithGravatar mohring2001-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1623 85f007b7-540e-0410-9357-904b9bb8a0f7
* entetesGravatar filliatr2001-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retire les parentheses autour des tactiquesGravatar mohring2000-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@766 85f007b7-540e-0410-9357-904b9bb8a0f7
* theories/RelationsGravatar filliatr2000-06-21
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@510 85f007b7-540e-0410-9357-904b9bb8a0f7