aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend.coq
Commit message (Collapse)AuthorAge
* nouveau module ZdivGravatar filliatr2002-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Elimination Elimdep.vGravatar mohring2002-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2570 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de ↵Gravatar letouzey2002-01-18
| | | | | | contrib/omega vers theories/ZArith git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2406 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr2001-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2281 85f007b7-540e-0410-9357-904b9bb8a0f7
* remise au gout du jour du repertoire theories/Sorting de la V6.3Gravatar letouzey2001-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2231 85f007b7-540e-0410-9357-904b9bb8a0f7
* Diverses petites simplications de la machine de preuves.Gravatar clrenard2001-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2204 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement des setoides.Gravatar clrenard2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1992 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de l'emplacement des fichiers pour les setoides.Gravatar clrenard2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1982 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de place et de nom de la tactique Setoid_rewrite.Gravatar clrenard2001-07-10
| | | | | | | Maintenant On appelle Rewrite et il choisit si c'est un setoide ou pas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1838 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise a jour des .dependGravatar clrenard2001-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1809 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajouts des theories du paradoxe de BerardiGravatar delahaye2001-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des entrees puor Setoid_replace.Gravatar clrenard2001-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1783 85f007b7-540e-0410-9357-904b9bb8a0f7
* Creation du fichier Zhints.v repertoriant les thms de ZArith et definissant ↵Gravatar herbelin2001-05-31
| | | | | | les thms interessants en hints git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1775 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de Rseries et Rtrigo_funGravatar mayero2001-04-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1686 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Fourier, DiscrR, ...Gravatar mayero2001-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1656 85f007b7-540e-0410-9357-904b9bb8a0f7
* support option -R pour coqdepGravatar filliatr2001-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1640 85f007b7-540e-0410-9357-904b9bb8a0f7
* Zarith -> ZArithGravatar filliatr2001-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1632 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de FieldGravatar delahaye2001-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1609 85f007b7-540e-0410-9357-904b9bb8a0f7
* branchement extraction en standard (pas de Require)Gravatar filliatr2001-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1561 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout lemmes arithmetiquesGravatar mohring2001-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1557 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4Gravatar filliatr2001-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1551 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added two files that are used for the connection with the graphical ↵Gravatar bertot2001-04-04
| | | | | | | | | user-interface pcoq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1542 85f007b7-540e-0410-9357-904b9bb8a0f7
* branchement extraction (bytecode seulement)Gravatar filliatr2001-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1509 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplification du make depend; fonctions de stat. util. memoire dans ↵Gravatar filliatr2001-02-08
| | | | | | certains modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
* calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)Gravatar filliatr2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1325 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1031 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@964 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de theories/WellfoundedGravatar filliatr2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@900 85f007b7-540e-0410-9357-904b9bb8a0f7
* separation calcul des implicites et declaration des constantes / inductifs / ↵Gravatar filliatr2000-11-21
| | | | | | variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@897 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@877 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr2000-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@853 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finalement PolyListSyntax est necessaire (la redondance venait d'une ↵Gravatar herbelin2000-11-10
| | | | | | confusion dans les methodes open/load) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@840 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de la table des tactic Definitions pour eviter l'ecritureGravatar mohring2000-11-07
| | | | | | | | | | de fonctions dans les .vo ajout de lemmes dans EqNat, Logic_Type suppression de PolyListSyntax qui redefinissait le Infix de append Recherche d'instances a reecrire dans les Cases et les FixPoint git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@820 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Few OCaml files in contrib/xmlGravatar sacerdot2000-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@798 85f007b7-540e-0410-9357-904b9bb8a0f7
* ntrefiner.ml* removed in module xmlGravatar sacerdot2000-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@762 85f007b7-540e-0410-9357-904b9bb8a0f7
* xml contribution added to the MakefileGravatar sacerdot2000-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@757 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour dependancesGravatar filliatr2000-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@613 85f007b7-540e-0410-9357-904b9bb8a0f7
* portage RefineGravatar filliatr2000-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@559 85f007b7-540e-0410-9357-904b9bb8a0f7
* portage EAuto et RingGravatar filliatr2000-06-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@513 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr2000-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@505 85f007b7-540e-0410-9357-904b9bb8a0f7
* portage Omega (mais toujours pas Zpower et Zlogarithm)Gravatar filliatr2000-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@400 85f007b7-540e-0410-9357-904b9bb8a0f7
* portage en ocaml / camlp4 3.00Gravatar filliatr2000-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@379 85f007b7-540e-0410-9357-904b9bb8a0f7
* TautoGravatar filliatr2000-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@331 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArithGravatar filliatr2000-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@327 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug discharge (work_alist contenanti plein de fois les memes choses)Gravatar filliatr2000-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@323 85f007b7-540e-0410-9357-904b9bb8a0f7
* compilation theories/ArithGravatar filliatr2000-03-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@312 85f007b7-540e-0410-9357-904b9bb8a0f7
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
| | | | | | | | | | - tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration diversesGravatar herbelin2000-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@269 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentationGravatar filliatr1999-12-13
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@245 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-15 07:46:51 +0000