aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-11-24majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4977 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-23MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4976 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-23MAJsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4975 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-23Prise en compte des definitions locales dans les (co-)points-fixesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4974 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-22Compatibiliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4973 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-22Traitement plus clair, notamment pour Locate, de quand quoter les ↵herbelin
composantes de notations + contournement du fait que Lexer arrive apres Symbol git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4972 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-22Bug introduit avec le 'Simpl f'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4971 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4970 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4969 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Suppression des niveaux videsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4968 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21ajout Pnat et Pcompare_antisymherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4967 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Ajout 'Simpl f'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4966 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Simplification; ajout Zcompare_antisymherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4965 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21ajout Pnat (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4964 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21ajout Pnat (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4963 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase ↵herbelin
et Pcompare_antisym git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4962 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Ajout Print Implicitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4961 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Tri et typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4960 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21MAJ format et docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4959 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Pas d'entrees autres que les predefinies en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4958 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4957 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-20Nouvelle solution pour le probleme d'effacement des niveaux vides de ↵herbelin
operconstr et pattern: plus de niveaux vides git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4956 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-20Code simplification in CCcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4955 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4954 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4953 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19ajout de Znumtheory.v dans ZArithletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4952 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19Restauration compatibilite 7.4 pour le Hint Unfold Rgtherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4951 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19Prise en compte renommagesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4950 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19Distinction entre 'as _' qui cache le terme filtre (si variable) et rien ↵herbelin
dans case_item git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4949 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19Deplacement subst_rawconstr dans Rawtermherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4948 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19Protection contre l'effacement des niveaux vides de operconstr et pattern ↵herbelin
par le delete_rule de camlp4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4947 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4946 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18correction suite ajout nouvelles tactiquesclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4945 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18reparation bug moins unaire (erreur de PP)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4944 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18.v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4943 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18tout clean-ide dans cleanherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4942 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4941 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Bug: faut brancher la sortie des tactiques sur stdout pendant traductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4940 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Mise en place systeme de qualification des noms renommes; Renommages dans ↵herbelin
Ring; Nouvelle redondance git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4939 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4938 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Blindage vis a vis des constructeurs partiellement appliquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4937 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Ajout mis_constructor_nargs_envherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4936 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Ajout recarg_lengthherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4935 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Un nouveau lemme redondant ...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4934 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Deplacement ZERO_le_inj dans Zorderherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4933 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Utilisation de la date cvs dans l'en-tete si make.result existeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4932 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18*** empty log message ***filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4931 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4930 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-17New tactics : econstructor, eleft, eright, esplitclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4929 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-17Bug affichage Hint Externherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4928 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-18 23:42:17 +0000