aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init
Commit message (Collapse)AuthorAge
* Une entrée spéciale "annot" pour les piquantsGravatar herbelin2002-12-15
| | | | | | | Positionnement du scope type_scope à certains endroits bien choisis git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3445 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout syntaxe '>'Gravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3444 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai d'introduction d'un scope des typesGravatar herbelin2002-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-échappement des \ et " dans les token stringGravatar herbelin2002-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3339 85f007b7-540e-0410-9357-904b9bb8a0f7
* SimplificationGravatar herbelin2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3328 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai de suppression du caractere d'echappement des stringGravatar herbelin2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3327 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de précisionsGravatar herbelin2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3315 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour sur associativité à droite de * pour compatibilité de prodGravatar herbelin2002-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3308 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ne pas cacher les Metas d'une notations, ils peuvent être liant dansGravatar herbelin2002-11-26
| | | | | | | les filtrage de ltac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3302 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus d'indication pour le gestionnaire de niveauxGravatar herbelin2002-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3292 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiquesGravatar herbelin2002-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3290 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug niveauGravatar herbelin2002-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3288 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retablissement SynDef Value/ErrorGravatar herbelin2002-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3278 85f007b7-540e-0410-9357-904b9bb8a0f7
* OubliGravatar herbelin2002-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3277 85f007b7-540e-0410-9357-904b9bb8a0f7
* Généralisation de l'utilisation de NotationGravatar herbelin2002-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3269 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les parenthèses de la notation '(n)' maintemant mises par ML pour un ↵Gravatar herbelin2002-11-20
| | | | | | meilleur affichage des entiers dans le scope nat_scope git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3261 85f007b7-540e-0410-9357-904b9bb8a0f7
* OubliGravatar herbelin2002-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3234 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' ↵Gravatar herbelin2002-11-07
| | | | | | comme un entier de nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3222 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourGravatar herbelin2002-10-23
| | | | | | | | compatibilité avec la surcharge dans certains développements (p.e. Utrecht/ABP) Déplacement de ~ au niveau 5 qui est le niveau des atomes propositionels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3175 85f007b7-540e-0410-9357-904b9bb8a0f7
* Redéplacement de + (sum) et * (prod) au niveau de + et * de ↵Gravatar herbelin2002-10-22
| | | | | | l'arithmétique; ajout d'une option 'level' pour Notation; utilisation de Notation pour sumor et sumbool git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3173 85f007b7-540e-0410-9357-904b9bb8a0f7
* Niveau d'affichage sumor/sumbool incohérent avec le parsingGravatar herbelin2002-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3166 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des délimiteurs dans les motifs de CasesGravatar herbelin2002-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3164 85f007b7-540e-0410-9357-904b9bb8a0f7
* Et 48, et 80, et 81, et 91, et 95, ... pour accommoder toujours plus de contribsGravatar herbelin2002-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3157 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs dans la factorisation des règles de parsing de "{ ... } * ..."Gravatar herbelin2002-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3156 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parsing des entiers de nat jusqu'à 29 pour accommoder certaines contribsGravatar herbelin2002-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3154 85f007b7-540e-0410-9357-904b9bb8a0f7
* La règle pour parser "(1)", "(2)", ... entre en conflit avec les expressionsGravatar herbelin2002-10-14
| | | | | | | de la forme "(1+...)" : remplacement par une approximation finie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3134 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'ensembles de notations symboliques pour nat, Z et RGravatar herbelin2002-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3125 85f007b7-540e-0410-9357-904b9bb8a0f7
* NettoyageGravatar herbelin2002-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3124 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de + et * aux niveaux de précédence 7 et 6Gravatar herbelin2002-10-13
| | | | | | | Utilisation du parseur de constr pour les productions des règles de syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3123 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de + et * aux niveaux de précédence 7 et 6Gravatar herbelin2002-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3122 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug de précédenceGravatar herbelin2002-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2869 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hack pour parser '{x:T|P}*B' sans parenthesesGravatar herbelin2002-07-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2857 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation d'Infix/Distfix autant que possibleGravatar herbelin2002-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2728 85f007b7-540e-0410-9357-904b9bb8a0f7
* petite erreur de syntaxeGravatar barras2002-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2683 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout des theoremes eqT_rec_r et eqT_rect_r pour RewriteGravatar barras2002-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2680 85f007b7-540e-0410-9357-904b9bb8a0f7
* lemmes plus_O_n et plus_Sn_m (pour Yves)Gravatar filliatr2002-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2672 85f007b7-540e-0410-9357-904b9bb8a0f7
* lemmes plus_O_n et plus_Sn_m (pour Yves)Gravatar filliatr2002-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2671 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
* DocGravatar herbelin2002-02-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2492 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation des theoremes dans Set et Type (def. de Acc_rect etGravatar barras2002-02-19
| | | | | | | well_founded_induction_type) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2485 85f007b7-540e-0410-9357-904b9bb8a0f7
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Syntaxe IF then else au lieu de either and_then or_elseGravatar barras2002-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2473 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement generation de schema d'elimination, False_rec est primitif, ↵Gravatar mohring2002-01-31
| | | | | | Constructor tac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2447 85f007b7-540e-0410-9357-904b9bb8a0f7
* modification de la definition des def inductives unitaires et autorisation ↵Gravatar mohring2002-01-29
| | | | | | d'elimination sur la sorte Type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2442 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifs incongrues dans le précédent commitGravatar herbelin2002-01-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2385 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ des Id pour coqwebGravatar herbelin2002-01-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression d'Export redondantsGravatar herbelin2001-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2190 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de Logic_Type.sigT, redondant avec Specif.sigTGravatar herbelin2001-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2139 85f007b7-540e-0410-9357-904b9bb8a0f7
* and_rec redondantGravatar letouzey2001-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2081 85f007b7-540e-0410-9357-904b9bb8a0f7
* TransparentGravatar barras2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 06:25:40 +0000