aboutsummaryrefslogtreecommitdiff
path: root/contrib/fourier
AgeCommit message (Collapse)Author
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2745 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2720 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-19un thm de plus dans Zdiv; un retour chariot apres un message de la tactique ↵filliatr
FourierR git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2659 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-07integration de field a fouriermayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1734 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Ajout Fouriermayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1657 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-19 22:15:28 +0000