aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2003-01-21Renommage dans Binomial.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3562 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-21Binome.v -> Binomial.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3560 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-21MAJ ArithPropdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3559 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-21Renommage dans AltSeries.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3558 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-21Renommage dans Alembert.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3557 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-21Quelques améliorationsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3556 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-21Suppression de INR2 / Conséquence logique de la nouvelle représentation ↵desmettr
des constantes entières git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3555 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-21Quelques optimisations...desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3554 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-20Cgt définition de platdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3549 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-20Amélioration de DiscrRdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3548 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-20Utilisation de 'Recursive' pour les tactiques récursivesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3545 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-20Utilisation de 'Recursive' pour les tactiques récursivesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3543 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Clear sur hypothese non definieherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-17Optimisations pour Sup et RComputedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3519 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Ajout de RComputedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3514 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Ajout de la tactique Supdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3513 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16renommage de TAF.v en MVT.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3511 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Correction d'un petit bug dans Sup0desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3509 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Renommage de RealsB en Rbasedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3508 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Renommage de Rbase.v en RIneq.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3507 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-15Nouvelle interprétation des nombres réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3499 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-06bit vectorsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3488 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-28Re-installation nombres dans les motifs sur Zherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3483 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-15Une entrée spéciale "annot" pour les piquantsherbelin
Positionnement du scope type_scope à certains endroits bien choisis git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3445 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-15Ajout syntaxe '>'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3444 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-15Ajout syntaxe '>'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3437 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-15Pas d'associativite pour =_Dherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3436 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-10Compatibilite times1 (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3415 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Nouvelle preuve de times_convert pour nouvelle définition de timesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3396 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-07Compatibilité times1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3387 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-06Un axiome en attendant la mise a jour de la preuve de times_convertherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3386 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-06Amélioration sensible de l'efficacité de la multiplicationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3384 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-03Essai d'introduction d'un scope des typesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3363 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Z_scope doit annuler l'affichage de = entreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3349 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-29Re-échappement des \ et " dans les token stringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3339 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Simplificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3328 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Essai de suppression du caractere d'echappement des stringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3327 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Plus de précisionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3315 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27cond_pos -> cond_positivity pour cause de conflit avec posreal...desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3313 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27Réorganisation de la librairie des réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3311 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27Retour sur associativité à droite de * pour compatibilité de prodherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3308 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Ne pas cacher les Metas d'une notations, ils peuvent être liant dansherbelin
les filtrage de ltac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3302 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26MAJdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3298 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Theorie 'light' des réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3297 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Explicitation de NONA car sinon LEFTA par défaut; déplacement dans 5herbelin
qui est le niveau des relations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3294 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Plus d'indication pour le gestionnaire de niveauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3292 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Correction affichage entiers en cas d'échecherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3291 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3290 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Bug niveauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3288 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25Rétablissement affichage des entiers de natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3279 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 05:31:49 +0000