aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
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-10-07 23:25:24 +0000