aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-11-13Niveau V8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4894 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13Fermeture de la section maintenant necessaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4893 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13factorisation et generalisation des clausesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13Passage a un SStream predicatifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4891 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4890 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13Requireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4889 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13qq petit ajouts à Zdivletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4888 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4887 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12MAJ INZherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4886 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4885 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Bug TacIdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4884 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Ajout lemme projectionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4883 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12%type au lieu de %Therbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4882 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Lemmes dans un sens plus naturelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4881 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Suppression du "..." final !herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4880 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Restructuration ZArithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4879 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4878 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Noms canoniques pour les variables lieesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4877 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Independance vis a vis noms variables liees; partie sur bool dans Zboolherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4876 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Noms/énoncés plus canoniquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4875 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Independance vis a vis noms variables lieesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4874 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Ajout lemmes; independance vis a vis noms variables liees; restructurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4873 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Ajout partie sur bool anciennement dans Zmischerbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4872 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Ajout lemmes; independance vis a vis noms variables lieesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4871 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Nouvelle et derniere vague de renommageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4870 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Prise en compte des alias syntaxiques vers des references dans divers lieux ↵herbelin
de globalisation des constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4869 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Mise en place systeme de renommage des noms de variables liees dans la ↵herbelin
bibliotheque standard; Renommage zarith_aux, fast_integer git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4868 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Mise en place systeme de renommage des noms de variables liees dans la ↵herbelin
bibliotheque standard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4867 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12MAJ ZArith; contraintes plus faibles pour decider la capacite a interpreter ↵herbelin
les numeraux git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4866 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Test de la reference principale plutot que le module dans lequel se trouve ↵herbelin
la reference pour l'interpretation des numeraux git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4865 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4864 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Idtac peut prendre un argument à affichernarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4863 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12On sait jamaisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4862 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12conseille l'utilisation de la release officielle 2.2.0 de lablgtkletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4861 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12petits changements de syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12deux doigts d'extraction dans le CHANGES pour la V8letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4859 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12les modifs depuis la 7.4letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4858 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12TODOletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4857 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Extraction Module M devient simplement Extraction Mletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4856 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-11majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4855 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10MAJ OTHERFLAGSherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4854 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10Re-suppression de is_verbose dans Print, pour coqideherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4853 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10Suppression SearchNamed finalement redondant avec SearchAboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4852 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10le pb du <<.v vu comme module>> engendre maintenant une erreurletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4851 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10message informant de l'ecriture d'un fichier extraitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4850 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10révision du traitement des axiomes non réalisésletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4849 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4848 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10essai d'extraction sous un moduleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4847 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Quelqes renommages lies a Zorderherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4846 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Ajout quelques lemmes; noms des variables lieesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4845 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 17:35:35 +0000