aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Prise en compte des defs syntaxiques dans is_global et global_reference qui ↵Gravatar herbelin2003-11-24
| | | | | | passent donc de Termops a Constrintern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4980 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renoncement de la compatibilite des noms qualifies au profit de la ↵Gravatar herbelin2003-11-24
| | | | | | compatibilite des arguments implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4979 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4978 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4977 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4976 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJsGravatar herbelin2003-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4975 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des definitions locales dans les (co-)points-fixesGravatar herbelin2003-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4974 85f007b7-540e-0410-9357-904b9bb8a0f7
* CompatibiliteGravatar herbelin2003-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4973 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traitement plus clair, notamment pour Locate, de quand quoter les ↵Gravatar herbelin2003-11-22
| | | | | | 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
* Bug introduit avec le 'Simpl f'Gravatar herbelin2003-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4971 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4970 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des niveaux videsGravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4968 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout Pnat et Pcompare_antisymGravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4967 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'Simpl f'Gravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4966 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplification; ajout Zcompare_antisymGravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4965 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout Pnat (suite)Gravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4964 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout Pnat (suite)Gravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4963 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase ↵Gravatar herbelin2003-11-21
| | | | | | et Pcompare_antisym git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4962 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Print ImplicitGravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tri et typoGravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4960 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ format et docGravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4959 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas d'entrees autres que les predefinies en v8Gravatar herbelin2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4958 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle solution pour le probleme d'effacement des niveaux vides de ↵Gravatar herbelin2003-11-20
| | | | | | 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
* Code simplification in CCGravatar corbinea2003-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4955 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4954 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4953 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de Znumtheory.v dans ZArithGravatar letouzey2003-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restauration compatibilite 7.4 pour le Hint Unfold RgtGravatar herbelin2003-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4951 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte renommagesGravatar herbelin2003-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4950 85f007b7-540e-0410-9357-904b9bb8a0f7
* Distinction entre 'as _' qui cache le terme filtre (si variable) et rien ↵Gravatar herbelin2003-11-19
| | | | | | dans case_item git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4949 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement subst_rawconstr dans RawtermGravatar herbelin2003-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4948 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre l'effacement des niveaux vides de operconstr et pattern ↵Gravatar herbelin2003-11-19
| | | | | | par le delete_rule de camlp4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4947 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4946 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction suite ajout nouvelles tactiquesGravatar clrenard2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4945 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation bug moins unaire (erreur de PP)Gravatar barras2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4944 85f007b7-540e-0410-9357-904b9bb8a0f7
* .v8Gravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4943 85f007b7-540e-0410-9357-904b9bb8a0f7
* tout clean-ide dans cleanGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4942 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4941 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug: faut brancher la sortie des tactiques sur stdout pendant traductionGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4940 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place systeme de qualification des noms renommes; Renommages dans ↵Gravatar herbelin2003-11-18
| | | | | | Ring; Nouvelle redondance git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4939 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mortGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4938 85f007b7-540e-0410-9357-904b9bb8a0f7
* Blindage vis a vis des constructeurs partiellement appliquesGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4937 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout mis_constructor_nargs_envGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout recarg_lengthGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4935 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un nouveau lemme redondant ...Gravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4934 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement ZERO_le_inj dans ZorderGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4933 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de la date cvs dans l'en-tete si make.result existeGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4932 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar filliatr2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4931 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 22:57:24 +0000