aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
AgeCommit message (Collapse)Author
2004-03-30Heuristique pour traduire if-then-else quand le re-typage echoueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5616 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-28Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ↵herbelin
sont supposes sans dependances en les arguments des constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5589 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14correction bug de facto des fix (2e)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5478 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14correction bug de facto des fixbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5477 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14correction bug de choix de noms courts avec Suresnes/BDDbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5476 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-08correction de bugs des points fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5440 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts ↵barras
fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-26Keep structure information for Fixpoint declaration and Fix termsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5386 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-18- fixed the Assert_failure error in kernel/modopsbarras
- fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-18Bug coercions imbriquees + suppression des coercions avant filtrage sur ↵herbelin
notations pour respecter le cpmt v7 et la symtrie avec le parsing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5357 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Correction bug affichage en presence de '{ _ }'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5323 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Décomposition automatique des règles d'analyse syntaxique pour lesherbelin
notations contenant le motif "{ _ }": permet de réperer des incohérences de précédence comme dans "A*{B}+{C}" en présence d'une notation "_ * { _ }" (il était parsé associant à droite au lieu de à gauche) et de supprimer les règles spécifiques de Notations pour parser "B+{x:A|P}" etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5319 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-03Relachement condition pour afficher @ en cas d'explicitation d'implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5285 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29Ajout option raw_print (Set Printing All) pour desactiver toute ↵herbelin
fonctionnalite de haut niveau de l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5269 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-27Bug activation erronée du traducteur en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5257 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-26reparation de qqs bugs du traducteurbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5248 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-21Traduction PolyList/List dans la qualificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5124 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-19Substitution dans REvar et PEvar plutot que encodage via noeud application ↵herbelin
pour eviter la confusion avec la (vraie) application git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5114 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-15'Eval' protege dans Ppconstrnew; eval n'a pas le meme besoinherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5098 85f007b7-540e-0410-9357-904b9bb8a0f7
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-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-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-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-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-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-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-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-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-09-30Les notations hors scope s'empilent maintenant comme des scopes neherbelin
contenant qu'une notation + renommage dans Reals git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4505 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Syntaxe plus liberale pour le type des arguments de filtrage du 'match'; ↵herbelin
traduction de noms git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4490 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Nouvelle serie de traductionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4482 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Changement de l'afficheur pour que les variables liées aient un nom ↵herbelin
indépendant des globaux quand hors but (on garde l'évitement des globaux en but, pour compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4458 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
extraction: pb avec les variables de section definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 17:03:58 +0000