aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* 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
* Pas de globalisation impérative pour les GrammarGravatar herbelin2002-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3361 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-déplacement du résultat de Grammar au niveau constr_expr (globalisation ↵Gravatar herbelin2002-12-02
| | | | | | uniquement des noms - sauf cases, fix, ..., pas d'implicites, pas d'interprétation des scopes - pas plus robuste qu'avant...); Diverses améliorations affichage et parsing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3352 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des options "Set Contextual Implicits" et "Set Strict ImplicitsGravatar herbelin2002-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3351 85f007b7-540e-0410-9357-904b9bb8a0f7
* On force l'associativité pour les entrées sans niveauxGravatar herbelin2002-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Raffinement syntaxe InfixGravatar herbelin2002-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3344 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affinement de la gestion des niveaux toujours; type ETBigintGravatar herbelin2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3334 85f007b7-540e-0410-9357-904b9bb8a0f7
* typo ?Gravatar letouzey2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3319 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affinement encoreGravatar herbelin2002-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout répertoire interpGravatar herbelin2002-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3310 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réaffichage des Syntactic Definition (printer constr_expr).Gravatar herbelin2002-11-26
| | | | | | | | Affinement de la gestion des niveaux de constr. Cablage en dur du parsing et de l'affichage des délimiteurs de scopes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Syntaxe delimiteursGravatar herbelin2002-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3283 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ delimiters et niveaux d'associativiteGravatar herbelin2002-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3281 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
* Autoriser les abbreviations de CasesGravatar herbelin2002-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3257 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage à une représentation des fixpoints plus primitive dans constr_expr ↵Gravatar herbelin2002-11-15
| | | | | | (càd avec indices) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3245 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
* Un Local construit par preuve hors section doit être considéré globalGravatar herbelin2002-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3216 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
| | | | | | | | | | | - Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle option -xml à coqtop pour compiler un développement enGravatar herbelin2002-11-05
| | | | | | | l'exportant au format xml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimisation du choix des niveaux intermédiaires dans une notation complexeGravatar herbelin2002-10-30
| | | | | | | Désagglutination du squelette de la notation et de sa précédence git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3196 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2002-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3182 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification changements autour de Remark/Fact/LocalGravatar herbelin2002-10-23
| | | | | | | Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3180 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le test de redondance d'une règle était trop fortGravatar herbelin2002-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3177 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
* 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
* Réparation du mécanisme des infixes quand ils commencent par une lettreGravatar herbelin2002-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3153 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 12:21:39 +0000