aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Collapse)AuthorAge
* Nettoyage suite à la détection par défaut des variables inutilisées par ↵Gravatar herbelin2005-11-08
| | | | | | ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 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
* improves shadows in the main windowGravatar narboux2005-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7232 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression de code commenteGravatar coq2005-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7103 85f007b7-540e-0410-9357-904b9bb8a0f7
* whelp + correction bug affichage de coqideGravatar coq2005-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7102 85f007b7-540e-0410-9357-904b9bb8a0f7
* Achèvement du déplacement de fonctionnalités unix et browser de ide vers libGravatar herbelin2005-05-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de fonctionnalités unix et browser de ide vers libGravatar herbelin2005-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7041 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 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
* Complétion déclarations coqideGravatar herbelin2004-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6362 85f007b7-540e-0410-9357-904b9bb8a0f7
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
* qq bugs du highlight de CoqIDEGravatar filliatr2004-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6267 85f007b7-540e-0410-9357-904b9bb8a0f7
* 2 bugs de reconnaissanceGravatar coq2004-10-15
| | | | | | | de fin de phrase corriges git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6218 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
* New command "Add Relation ..." (for the new implementation of setoid_*).Gravatar sacerdot2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6048 85f007b7-540e-0410-9357-904b9bb8a0f7
* "Print Setoids" command added.Gravatar sacerdot2004-07-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5968 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction vis a vis du type loc pour ocaml 3.08Gravatar herbelin2004-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5951 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
* added commands to ideGravatar corbinea2004-07-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5870 85f007b7-540e-0410-9357-904b9bb8a0f7
* but autoamtics tactics savingGravatar marche2004-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5723 85f007b7-540e-0410-9357-904b9bb8a0f7
* Achèvement du passage des emprunts à cameleon de Maxence Guesdon de la ↵Gravatar herbelin2004-04-30
| | | | | | version 1.2 (QPL) à la version 1.3 (GPL) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5717 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout codingGravatar herbelin2004-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5671 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage a la version 1.3 sous GPL des outils okey et configwin de cameleon ↵Gravatar herbelin2004-04-13
| | | | | | en remplacement de la version 1.2 qui etait sous QPL git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5670 85f007b7-540e-0410-9357-904b9bb8a0f7
* warning dialog when save failsGravatar marche2004-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5641 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour des menusGravatar mohring2004-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5507 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout des Print Scopes dans liste commandes sans effetGravatar mohring2004-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5493 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
* bug fix find coqideGravatar coq2004-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5290 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
* search windowGravatar coq2004-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5288 85f007b7-540e-0410-9357-904b9bb8a0f7
* pour ide sous windowsGravatar coq2004-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5267 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide utf8Gravatar marche2004-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5222 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
* commandes de coqideGravatar marche2003-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5081 85f007b7-540e-0410-9357-904b9bb8a0f7
* preferencesGravatar marche2003-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5077 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug de preferencs/font"Gravatar marche2003-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5076 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
* power associe a droiteGravatar marche2003-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5072 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
* contrib jcfGravatar marche2003-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5053 85f007b7-540e-0410-9357-904b9bb8a0f7
* commands renomme en queries, command goto a la place de forward to backwardt oGravatar marche2003-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5015 85f007b7-540e-0410-9357-904b9bb8a0f7
* textesGravatar marche2003-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4986 85f007b7-540e-0410-9357-904b9bb8a0f7
* aboutGravatar marche2003-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4983 85f007b7-540e-0410-9357-904b9bb8a0f7
* tentative de completion ESC-/ a la emacsGravatar letouzey2003-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4981 85f007b7-540e-0410-9357-904b9bb8a0f7
* .v8Gravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4943 85f007b7-540e-0410-9357-904b9bb8a0f7