aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.ml
Commit message (Collapse)AuthorAge
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
| | | | | | | | | devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
* add visibility of extraction messages in coqideGravatar letouzey2007-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10230 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 1716: Scheme now print the right messagesGravatar vsiles2007-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10175 85f007b7-540e-0410-9357-904b9bb8a0f7
* fin des conclusions multiplesGravatar corbinea2007-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | delta-reduction at fonctor application. Example: Module Type S. Parameter Inline N : Set. End S. Module F (X:S). Definition t := X.N. End F. Module M. Definition N := nat. End M. Module G := F M. Print G.t. G.t = nat : Set git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7
* decl mode: anonymous factsGravatar corbinea2007-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9534 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed same_file (#1141)Gravatar barras2006-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9263 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: affichage des sous-buts et hypothèses et métas comme types deGravatar herbelin2006-10-19
| | | | | | | | | telle sorte que les coercions vers sortclass ne soient pas affichées (comme dans coqtop) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9249 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit 9110 (uniformisation position notation dans les blocs inductifs)Gravatar herbelin2006-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9113 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications dans les scripts de configuration (coqtop et coqide affichent ↵Gravatar notin2006-07-28
| | | | | | maintenant le numéro de révision svn) + correction problème OCaml 3.07 et caml_;odify git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9063 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement VernacDebug par VernacSetOption (suite)Gravatar herbelin2006-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9024 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de l'option -where: on vérifie si la variable d'environnement ↵Gravatar notin2006-06-07
| | | | | | COQLIB est définie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8912 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #990 (LoadPath et option -R de coqideGravatar notin2006-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
| | | | | | | et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug de coqide sous windows (bad file descriptor)Gravatar barras2005-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Types inductifs parametriquesGravatar mohring2005-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Module/Declare Module syntax made more uniform:Gravatar sacerdot2005-01-06
| | | | | | | | | | | | | | | | | * "Module X [binders] [:T] [:= b]." is now used to define a module both in module definitions and module type definitions. Moreover "b" can now be a functor application in every situation (this was not accepted for module definitions in module type definitions) * "Declare Module X : T." is now used to declare a module both in module definitions and module type definitions. - Added syntactic sugar "Declare Module Export/Import" and "Module Export/Import" - Added syntactic sugar "Module M(Export/Import X Y: T)" and "Module Type M(Export/Import X Y: T)" (only for interactive definitions) (doc TODO) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6564 85f007b7-540e-0410-9357-904b9bb8a0f7
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* ide: silent behavior better, save icon, -byte worksGravatar marche2004-03-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5427 85f007b7-540e-0410-9357-904b9bb8a0f7
* Localisation des erreurs d'internalisation des notations de tactiquesGravatar herbelin2004-02-12
| | | | | | | | dans le module de leur définition. Error_in_file dans Util et étendu avec possibilité de noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 85f007b7-540e-0410-9357-904b9bb8a0f7
* highlightGravatar marche2004-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5289 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables ↵Gravatar herbelin2004-01-13
| | | | | | a b:A' et 'Variables (a:A) (b:A)' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5198 85f007b7-540e-0410-9357-904b9bb8a0f7
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
* ameliorations coqideGravatar coq2003-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5161 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide menus on golasGravatar marche2003-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5104 85f007b7-540e-0410-9357-904b9bb8a0f7
* plus de syntaxe v8Gravatar marche2003-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5089 85f007b7-540e-0410-9357-904b9bb8a0f7
* pas de Goal pendant une preuveGravatar filliatr2003-12-08
| | | | | | | pas de Debug On/Off git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5075 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement menu et toolbarGravatar marche2003-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Conjecture declare maintenant un axiome; reorganisation VernacDefinitionGravatar herbelin2003-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4710 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement next_global_ident_away dans TermopsGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4611 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide : les nouveaute d'aoutGravatar monate2003-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4424 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: fixed problems with -R -I and coqide interactionGravatar monate2003-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4237 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide : status bar more informative, forbid Section/Module in proo modeGravatar monate2003-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4208 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: undo plus efficace sur les inductifsGravatar filliatr2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4157 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: about now displays versions/Fix for alt-enterGravatar monate2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4147 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: undo immediat sur les commandes ne modifiant pas l'etatGravatar filliatr2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4145 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: blaster interruptibleGravatar monate2003-05-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4082 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: blaster V1Gravatar monate2003-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4059 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar monate2003-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4031 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIde : but reset_modGravatar filliatr2003-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4030 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: load/save file encoding support/Gravatar monate2003-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4021 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: toolbar/autosaveGravatar monate2003-05-07
| | | | | | | | | Hugo: Suppression du type dans les notations == et <> entre Suppression du type dans les notations == et <> entre volution second traducteur selon discussion TYPES git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3993 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: bugfix du C-C pendant Undo+paren_highlightGravatar monate2003-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3798 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: efficacite des buts etc...Gravatar monate2003-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3795 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: locale iso-8859-1 par defaut si probleme. Interdiction des lemmes ↵Gravatar monate2003-03-26
| | | | | | locaux. Reparation du Undo avec Section et constantes de meme nom. Decoupe tag modifie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3793 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: addloadpath corrigeGravatar monate2003-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3792 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: maj commandesGravatar monate2003-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3766 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIde: Install.ide Revert bugfix.Gravatar monate2003-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3741 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 14:45:00 +0000