aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-10-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@782 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-28Clarification message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@781 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@780 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27Passage command -> constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@779 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27Simpl fait trop maintenant; faut adapterherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@778 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27erreur dans intro_gen corrigéefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@777 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27Chasse au Cast de Castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@776 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27Intro choue si le nom d'hypothse existe au lieu de mettre un avertissementherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@775 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27Ajoute : Ast dans la regle de grammairemayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@774 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27g_natsyntax et g_zsyntax maintenant toujours linkesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@773 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27Mise a jour TheoryListmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@772 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@771 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26Essai de remplacement du whd_betaiotaevar de Qed par un whd_iseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@770 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26Suppression cas Cast dans whd_ise et whd_ise1; Suppression du cast au moment ↵herbelin
de l'instanciation des Meta dans plain_instance git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@769 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26Require Export recursifsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@768 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26Semi_Ring_Theory_of decommentemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@767 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26Retire les parentheses autour des tactiquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@766 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26Ajout de la mthode load_function pour exporter les 'tactic-ring-theory'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@765 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26Bug Simpl avec Cases cache sous plusieurs constantesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@764 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26Renommage var en named et decl en assumherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@763 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26ntrefiner.ml* removed in module xmlsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@762 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-25Manquait le cas Constr de dyn_polynomherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@761 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-25Bug pop_path_prefix : List.rev manquantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@760 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-25Porting from V6 finished, but not working.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@759 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-25Added xml contribution to configuresacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@758 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-25xml contribution added to the Makefilesacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@757 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-25xml contribution created.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@756 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@755 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24Changement des analyseurs syntaxiques de Grammar et Syntaxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@754 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24un espaceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@753 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24Syntaxe des tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@752 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24Renommage command -> constr et changement des analyseurs syntaxiques de ↵herbelin
Grammar et Syntax git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@751 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24Bug réduction suite modifs let-inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@750 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24Meilleur endroit pour déclarer les parseurs de grammaires et joli affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@749 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24Bug de copier-collerherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@748 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@747 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23Modifications pour implicites améliorésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@746 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23Rétablissement compatibilité des implicites (2ème) (mais amélioration)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@745 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@744 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23Import de Infix au Requireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@743 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@742 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@741 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23L'état implicite des définitions survivant au discharge redevient celui du ↵herbelin
moment de la définition (et non celui du moment de la fermeture de section) mais les args imps sont recalculés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@740 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23module_segment et module_filenamefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@739 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23La réduction du Let s'appelle maintenant zeta comme dans le lambda-mu-calculherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@738 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23Simplifications/questionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@737 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@736 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23Petit nettoyage de Evarutil et Evarconvherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@735 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-21Bug indices dans l'instance d'une evarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@734 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-21Pb affichage warningherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@733 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-26 09:10:21 +0000