aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* Ajout option -v8 à coqtopnew pour permettre le changement de comportement ↵Gravatar herbelin2003-04-09
| | | | | | des implicites (passage au mode strict) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3882 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation de Impargs + mise en place d'une infrastructureGravatar herbelin2003-04-09
| | | | | | | | (notatemment des tables de parsing et d'affichage différenciées) permettant au traducteur de changer les implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3874 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte affichage coercions traducteur dans ConstrexternGravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3873 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option "Local" à "Open Scope"Gravatar herbelin2003-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3867 85f007b7-540e-0410-9357-904b9bb8a0f7
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
| | | | | | | | | pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
* Options d'affichage maintenant dans ConstrexternGravatar herbelin2003-04-07
| | | | | | | Ajout "Set/Unset Printing Implicits" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3846 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un choix 'onlyparse'Gravatar herbelin2003-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3822 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restauration de make_all_different (disparu depuis version 1.74) car sinon ↵Gravatar herbelin2003-03-31
| | | | | | detype echoue sur les variables anonymes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3819 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implicit Variables Type dans les inductiveGravatar herbelin2003-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3808 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de Set Print WidthGravatar gregoire2003-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3790 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2003-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3764 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
* tous les fichiers passes a Coq IDEGravatar filliatr2003-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3735 85f007b7-540e-0410-9357-904b9bb8a0f7
* fichiers sur la ligne de commande passes a Coq IDEGravatar filliatr2003-03-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3728 85f007b7-540e-0410-9357-904b9bb8a0f7
* Recuperation des outputs de l'interpretation des commandes vernac et des ↵Gravatar desmettr2003-02-28
| | | | | | erreurs pour le traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3721 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le lexeur et Notation savent reconnaître si un unicode des blocsGravatar herbelin2003-02-27
| | | | | | | | | | 0380-03FF (lettres grecques) 2100-214F (symboles assimilés à des lettres), 2200-22FF (opérateurs mathématiques), 2300-23FF (symboles techniques divers) et 2600-26FF (symboles divers) est un caractère spécial ou non lorsque encodé en utf-8. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3712 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test de non bouclage malencontreux dans les niveauxGravatar herbelin2003-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Chargement dynamique de .cmaGravatar delahaye2003-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3676 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debugger plus informatifGravatar delahaye2003-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Undo dans Coq IDEGravatar filliatr2003-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3673 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du traducteurGravatar desmettr2003-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3664 85f007b7-540e-0410-9357-904b9bb8a0f7
* interface GTK2 experimentaleGravatar monate2003-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3660 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour satisfaire ProofGeneralGravatar coq2003-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3634 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement de place du Initial State (maintenant apres l'analyse de la ligne ↵Gravatar filliatr2003-01-30
| | | | | | de commande) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3627 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement du test 'il reste des preuves en cours'Gravatar filliatr2003-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3544 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration interpréteur de tactique: plus d'évaluation partielle à ↵Gravatar herbelin2003-01-19
| | | | | | la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3532 85f007b7-540e-0410-9357-904b9bb8a0f7
* msg Failtac; echec -batch s'il reste des preuvesGravatar filliatr2003-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3525 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs affichageGravatar herbelin2003-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3517 85f007b7-540e-0410-9357-904b9bb8a0f7
* -emacs: plus de prompt entre les lignesGravatar filliatr2003-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3510 85f007b7-540e-0410-9357-904b9bb8a0f7
* Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à ↵Gravatar herbelin2003-01-15
| | | | | | une sorte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export M + Module M <: SIGGravatar coq2003-01-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3494 85f007b7-540e-0410-9357-904b9bb8a0f7
* SearchAboutGravatar filliatr2003-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3489 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration règles d'affichageGravatar herbelin2002-12-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3487 85f007b7-540e-0410-9357-904b9bb8a0f7
* Légère amélioration des messages d'erreur des with-bindings et des RewriteGravatar herbelin2002-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affinement affichageGravatar herbelin2002-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3471 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit netoyage dans libGravatar coq2002-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite du commit precedentGravatar barras2002-12-19
| | | | | | | | - amelioration des messages d'erreurs de la condition de garde - reorganisation de clenv.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3457 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des scopes traversés dans les notationsGravatar herbelin2002-12-15
| | | | | | | | Traitement spécial pour le scope type_scope à l'internalisation Ajout "Locate Notation" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3441 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du vernac Proof withGravatar gregoire2002-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3425 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout options -v7 et -v8, et commandes V7only et V8onlyGravatar herbelin2002-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3418 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout options -v7 et -v8, et commandes V7only et V8onlyGravatar herbelin2002-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3407 85f007b7-540e-0410-9357-904b9bb8a0f7
* Problèmes et améliorations divers affichageGravatar herbelin2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3394 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mort ?Gravatar herbelin2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3391 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction divers bugs d'affichage; explicitation du niveau de grammaire ↵Gravatar herbelin2002-12-04
| | | | | | quand mentionn explicitement par l'utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3378 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction divers bugs d'affichage; explicitation du niveau de grammaire ↵Gravatar herbelin2002-12-04
| | | | | | quand mentionn explicitement par l'utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3377 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification Require FromGravatar mohring2002-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3376 85f007b7-540e-0410-9357-904b9bb8a0f7
* la table PARAMETER n'existe plus (mergé dans la table CONSTANT)Gravatar letouzey2002-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3369 85f007b7-540e-0410-9357-904b9bb8a0f7
* Préparation à la prise en compte des changements de scopes internes aux ↵Gravatar herbelin2002-12-03
| | | | | | notations; bugs d'affichage (confusion key/scope dans les délimiteurs); bug de non-indépendance des règles d'affichage et parsing vis à vis du nom des variables de la notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3365 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-26 02:45:27 +0000