aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-21Make sure pcoq will also display hypotheses with a value.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3553 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-21Add a few operators in the new version of xlate.ml and make surebertot
that ast_to_ct is not use anymore in translate_constr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3552 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-21majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3551 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-20Mauvaise interprétatin de IdentArgTypeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3550 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-20*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3547 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-20Protection contre les noms de tactiques inconnus; restriction exceptions ↵herbelin
rattrapées dans les Match git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3546 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-20deplacement du test 'il reste des preuves en cours'filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3544 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-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3542 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-20MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3541 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-20Petits bugsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3540 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Tests ltacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3539 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Il ne doit plus y avoir de preuves non terminées à la sortie du fichierherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3538 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Simplification de Simplify (plus de ())herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3537 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19MAJ Ltacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3536 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Utilisation d'une exception 'catchable'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3535 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-19Restructuration interpréteur de tactique: plus d'évaluation partielle à ↵herbelin
la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3533 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Restructuration interpréteur de tactique: plus d'évaluation partielle à ↵herbelin
la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3532 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Ajout pptacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3531 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Erreur sur precedent commitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3530 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Restructuration interpréteur de tactique: plus d'évaluation partielle à ↵herbelin
la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3529 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Localisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3528 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Rétablissement pr_patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3527 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-18majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3526 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-17msg Failtac; echec -batch s'il reste des preuvesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3525 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-17V7.4mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3524 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-17*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3523 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-17Version V7.4mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3522 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-17Mise a jour pour distribmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3521 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-17*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3520 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-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3518 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Bugs affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3517 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3516 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16Subst sur une hyp qui n'existe pas ne fait pas une anomaliebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3515 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-16*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3512 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-16-emacs: plus de prompt entre les lignesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3510 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-16majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3506 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 22:36:53 +0000