aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2003-10-31majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4747 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-30Redirected some of the verbose jprover output through the Pp module.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4746 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-30Affichage des negatifs au niveau de l'application, et des positifs au dessus ↵herbelin
du niveau du moins unaire git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4744 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-30traduction des noms de correctnessherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4743 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 22:55:12 +0000