aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-11-05Renommage canonique d'un lemme redondantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4799 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Branchement de Show Script sur l'afficheur structureherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4798 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Amelioration de l'afficheur de script structureherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4797 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4796 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-04En v8, une notation, c'est 2 regles et un niveauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4795 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-04Amelioration message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4794 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-04*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4793 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-04Explicitation message d'erreur nombres negatifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4792 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-04Pour eviter des anomalies au lieu d'erreur en mode traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4791 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-04Amelioration message d'erreur pour ltacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4789 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-04Amelioration message d'erreur avec pretyping; prise en compte syntactic def ↵herbelin
dans Unfold git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4788 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-04pour que make clean efface ide/utf8_convert.ml venant d'un .mllletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4786 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-03Check en plus parmi les keywordsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4785 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-03Exporting ^; utilisation arg scope impliciteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4783 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-03Compatibilite V7.4 pour le delimiteur de positiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4782 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4781 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4780 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Renforcement significatif du resultat principalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4779 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Rien de bien importantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4778 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4777 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4776 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Le printeur de Show Script n'etait pas le bon en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4775 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4774 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Ajout Diaconescu.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4773 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02AC + EXT -> EMherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4772 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Relations entre le choix (forme relationnelle) avec restriction ou nonherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4771 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Renommage bool en boolP pour eviter la qualificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4770 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Restauration preference Rge a Rle pour compatibilite...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4769 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Restauration preference Rge a Rle pour compatibilite...; petit nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4768 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Protection contre les buts sans inegaliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4767 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Ajout CPatNotation, PrintVisibilityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4766 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-01Fusion de l'univers et du nom d'entree en un 'Print Grammar entry' en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4763 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Il ne faut pas mettre le constrarg des tactiques au niveau lconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4762 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@4761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Traduction des noms pour les refs de pr_glob_generic (via pr_global)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4760 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Utilisation de niveaux pour l'extensibilite de la grammaires des patternsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4759 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Extension de get_constr_entry et symbol_of_production pour gerer les ↵herbelin
extensions de la grammaire des motifs de Cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4758 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Pas de defaut a 1 et LeftA pour les infixes v8; fusion de l'univers et du ↵herbelin
nom d'entree en un 'Print Grammar entry' en v8 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4757 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-01Finalement, niveau 0 pour l'argument du '-' unaire, pour éviter queherbelin
les entiers positifs soient parenthésés en tant qu'arguments de fonction; tant pis, il faudra écrire '-(-x)' au lieu de '--x' Ajout CPatNotation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4754 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-11-01Interdiction de nommer un object de nom commencant par Coq en dehors de la ↵herbelin
bibliotheque standard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4752 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les ↵herbelin
entiers positifs soient parentheses en tant qu'arguments de fonction; tant pis, il faudra ecrire '-(-x)' au lieu de '--x' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4751 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les ↵herbelin
entiers positifs soient parentheses en tant qu'arguments de fonction; tant pis, il faudra ecrire '-(-x)' au lieu de '--x'; suppression notations - et / unaire en V7 pour compatibilite V7.4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4750 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Heritage des notations v7 seulement si zero information v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4749 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Debranchement de Print si pas verbose (necessaire pour traducteur)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4748 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 09:22:59 +0000