aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Collapse)Author
2003-11-29Renommages discrets dans RIneq et Znumtheoryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5017 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-27Suite commit precedentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5011 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-27Qualification des noms utilisateurs en cas de collision avec un nom nouveauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5009 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26Traduction de @; simplification traduction des identherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5001 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25modif lexer: ident peut commencer par _barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4991 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-24Prise en compte des defs syntaxiques dans is_global et global_reference qui ↵herbelin
passent donc de Termops a Constrintern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4980 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-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-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-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-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-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-17Un ident filtre est liant seulement si une variable deja liee (sinon bug ↵herbelin
dans les Notation avec Cases - en particulier) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4926 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-16Bug filtrage pour inversion notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4924 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Conflit renommageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4913 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Oublis dans les rennomagesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4910 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Suppression renommages dans Peanoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4900 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13moins unaire au niveau 35, tactiques simple_induction et simple_destruct, ↵barras
Local devient Let git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4897 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-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-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-05Nouvelle vague de renommageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4804 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-04Extension de zarithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4790 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Extensibilite de la grammaires des patternsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4765 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Renommage Topconstr.map_aconstr_with_binders_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4764 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Ajout notations pour motifs de Cases; renommage map_aconstr_with_binders_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4756 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Ajout CPatNotation; renommage map_aconstr_with_binders_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4755 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ↵herbelin
dans la biblio standard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4753 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-30Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ↵herbelin
associative a gauche; gestion du signe dans le parseur pas dans l'interpreteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Ajout de Print Visibilityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4733 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-27Nouveaux renommages; mot-cle 'exists'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4717 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Nouveaux renommages; Traduction speciale pour 'length nil'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4693 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Optimisation de gen_constant_in_modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4689 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Bug Locate Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4684 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-17Re-desactivation de l'affichage des projectionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4668 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16print_projections a true juste pour le bench nocturneherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4660 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4652 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Debranchement de l'affichage systematique des projections avec la notation ↵herbelin
pointee; soumis maintenant a l'activation de l'option 'Set Printing Projections' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4651 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Debranchement de l'affichage systematique des projections avec la notation ↵herbelin
pointee; soumis maintenant a l'activation de l'option 'Set Printing Projections' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4649 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-15Gestion encore plus affinee des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4641 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Gestion affinee des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4637 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Nouvelles traductions de noms; mot-cle; affichage implicites par le traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4636 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14identityT = identityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4633 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles ↵herbelin
entrees pour Metasyntax git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4631 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10identity est equivalent sur Type (sauf sans argument)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4592 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10changement nouvelle syntaxe (pt fixes)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Pb residuel avec la prise en compte des parametres implicites d'inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4549 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Prise en compte des paramètres implicites d'inductifs pour la globalisation ↵herbelin
des types de constructeur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4548 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-01cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4510 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 05:56:46 +0000