aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
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
* Ajout syntaxe '>'Gravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3437 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas d'associativite pour =_DGravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3436 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilite times1 (suite)Gravatar herbelin2002-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle preuve de times_convert pour nouvelle définition de timesGravatar herbelin2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3396 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité times1Gravatar herbelin2002-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3387 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un axiome en attendant la mise a jour de la preuve de times_convertGravatar herbelin2002-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3386 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration sensible de l'efficacité de la multiplicationGravatar herbelin2002-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3384 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
* Z_scope doit annuler l'affichage de = entreGravatar herbelin2002-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3349 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
* cond_pos -> cond_positivity pour cause de conflit avec posreal...Gravatar desmettr2002-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3313 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation de la librairie des réelsGravatar desmettr2002-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3311 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
* MAJGravatar desmettr2002-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3298 85f007b7-540e-0410-9357-904b9bb8a0f7
* Theorie 'light' des réelsGravatar desmettr2002-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3297 85f007b7-540e-0410-9357-904b9bb8a0f7
* Explicitation de NONA car sinon LEFTA par défaut; déplacement dans 5Gravatar herbelin2002-11-26
| | | | | | | qui est le niveau des relations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3294 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
* Correction affichage entiers en cas d'échecGravatar herbelin2002-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3291 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
* Rétablissement affichage des entiers de natGravatar herbelin2002-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3279 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
* Traitement des parenthèses de nat au niveau du printerGravatar herbelin2002-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3273 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; ↵Gravatar herbelin2002-11-24
| | | | | | améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 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
* Remplacement de Syntactic Definition par NotationGravatar herbelin2002-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3267 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
* Definition et proprietes de l'integrale de RiemannGravatar desmettr2002-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3251 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proprietes des fonctions en escalierGravatar desmettr2002-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3250 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
| | | | | | | | | | | | | | | - Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 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
* JMeq now treated as an equality by tactics.Gravatar courant2002-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3232 85f007b7-540e-0410-9357-904b9bb8a0f7
* nettoyage preuve limit_compGravatar courant2002-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3231 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) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3176 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
* Mise en transparence des schémas d'induction bien-fondée sur SetGravatar herbelin2002-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3168 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 11:30:29 +0000