aboutsummaryrefslogtreecommitdiff
path: root/theories/Lists
AgeCommit message (Collapse)Author
2002-04-17*** empty log message ***werner
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2656 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-13Ajout de lemmesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2530 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-22Doc + ajout fold_symmetric et nth_Inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2493 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14option -dump-glob pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-03interversion de deux Elim dans In_dec pour que la fonction extraite soit ↵letouzey
efficace git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2156 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-29ajout option , Exc --> option, et lemmes dans les theoriesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1914 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-13Rétablissement nom de section Map après résolution bugs surcharge de nomsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1898 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1880 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-16modif Map sectionmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1851 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Library doc adjustments (until page 140)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1655 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Ajout de fonctions proposees par Cuiht Alvaradomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1630 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Mise de (*i autour CVS infomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1620 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-11documentation automatique de la bibliothèque standardfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-01- coqc : option -imagefilliatr
- coqmktop : manquaient des -I - tauto : rétablissement du vieux tauto en attendant la stabilité du nouveau - correction d'un bug de Simpl avec Fix (découvert dans preuve FTA) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1304 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-11Mise a jour Rbasemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1241 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-09Meta Definition -> Tactic Definitiondelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1239 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-09Tactic Definition -> Meta Definitiondelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1237 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Renommages autour de NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1147 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Elimination du 'delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1000 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Le nouvel Induction s'appelle NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@965 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24Petite simplif due au nouveau Tautodelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@939 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-13Retour a la version 1.1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@848 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Modification de la table des tactic Definitions pour eviter l'ecrituremohring
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
2000-11-07Orthographeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@813 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27Mise a jour TheoryListmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@772 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-05Remplacement de la tactique Program (partiel)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@659 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-20portage Refinefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@559 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-03Traduction de syntaxe vers ltacdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@551 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Retrait des parenthèses inutiles autour des tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@543 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21theories/Listsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@508 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-16 08:07:17 +0000