aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2003-10-29*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4742 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-29Choix sous sa forme relationnelleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4741 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4740 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4739 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Ordre (symbolique) des Requireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4738 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Passage de la notations de paire dans core_scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4737 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Passage des notations de type dans type_scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4736 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Ajout notations pour les expressions dans un anneauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4735 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Simplification preuveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4734 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-28Ajout %core; MAJ niveau connecteurs logiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4732 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Affichage Assert_failure en ocaml 3.07herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4731 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Message inductive largeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4730 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Nouveaux fichiers dans Logicherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4729 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Nouveaux fichiers dans Logic; prise en compte de l'option ↵herbelin
-strongly-classical la compilation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4728 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Options -strongly-constructive et -strongly-classicalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4727 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Set devient predicatif par defautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4726 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4725 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Fichier offrant l'axiome du choix unique en presence de logique classiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4724 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Fichier offrant l'axiome du choix en presence de logique classiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4723 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28La logique sur Type inclut celle sur Setherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4722 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Retour en arriere sur d'autres renommages de variablesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4721 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 09:11:26 +0000