aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Collapse)Author
2001-10-24Suppression de Logic_Type.sigT, redondant avec Specif.sigTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2139 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-27and_rec redondantletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2081 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Transparentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Deplacement des setoides.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1992 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18Modification de l'emplacement des fichiers pour les setoides.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1982 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-30Fin de la modif Exc/optionmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1917 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-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-05-29Correction d'un bug du pretty-printclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1770 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-15Modification pour passage p-automatesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1753 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-30Introduction d'une preuve de False_recmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1507 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
2000-12-21Bug d'affichage à cause des << ... >>herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1182 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21separation calcul des implicites et declaration des constantes / inductifs / ↵filliatr
variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@897 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Bug dans la règle de syntaxe de ex2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@867 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-07Changement/extension dans les noms de parseurs de Grammarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@816 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Parsing des motifs de Syntax avec la grammaire associée à l'univers de la ↵herbelin
déclaration (constr, tactic ou vernac) au lieu de ast (comme cela a été fait pour Grammar) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@721 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-28Plus de piquants dans les actions des grammaires; nom de la grammaire pris ↵herbelin
comme parseur par defaut; le type List devient AstList git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@575 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-30Bug affichage Error et Valueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@388 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-10t -> $t dans regle grammaire EXfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@313 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
- 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
2000-01-07Renommage command en constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@267 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-16erreurs de syntax :$filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@261 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13 - méthode load sur les Hintsfilliatr
- CAST pris en compte dans Astterm - Coercin.lookup_path_to_sort_from protégé par un try/with git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@248 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-13fichiers prelude Coqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@243 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 23:06:27 +0000