aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
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-07-20portage Refinefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@559 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-04correctionmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@554 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-03ajoutsmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@553 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-01Séparation des caractères spéciaux par un blancherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@544 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-21Require Plus ajoutefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@515 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21theories/Realsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@511 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21theories/Relationsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@510 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21theories/Setsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@509 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
2000-05-22Séparation des tokens -> et ~herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@468 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-22Changement nommage des hypothèses; parenthèses pour les tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@462 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-22Parenthèsesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@457 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18parethèses de tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@454 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03Ajout du langage de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-02portage Omega (mais toujours pas Zpower et Zlogarithm)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@400 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-04-26suppression doublonfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@375 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-30erreurs lexicales dans les patterns (manquait des espaces)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@359 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21 - bug make_module_marker (plus de # et de .obj maintenant)filliatr
- portage (partiel) de Zarith - bug discrEverywhere (manquait un "fun gls ->") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@353 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Retour sur les anciens nomsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@348 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-21Eqdep_dec retrouve ses noms d'origine grace au nouvel Reduction.instance ↵herbelin
utilisé par clenv git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@344 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-18Zarithfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@326 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-18g_natsyntax.mlfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@324 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-16Syntactic Definition n'etaient pas correctemenet importeesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@320 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-16mise sous CVSfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@318 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-03-10mise sous CVS du repertoire theories/Arithfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@311 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-10*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@310 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-07-06 14:11:07 +0000