aboutsummaryrefslogtreecommitdiff
path: root/ide
AgeCommit message (Collapse)Author
2005-06-03suppression de code commentecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7103 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-03whelp + correction bug affichage de coqidecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7102 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20Achèvement du déplacement de fonctionnalités unix et browser de ide vers libherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7046 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-19Déplacement de fonctionnalités unix et browser de ide vers libherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7041 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Compatibilité ocamlweb pour cible docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-06- Module/Declare Module syntax made more uniform:sacerdot
* "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
2004-11-27Complétion déclarations coqideherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6362 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17New command "Print Rewrite HindDb dbname".sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-28qq bugs du highlight de CoqIDEfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6267 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-152 bugs de reconnaissancecoq
de fin de phrase corriges git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6218 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-17restructuration des printers: proofs passe avant parsingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03New command "Add Relation ..." (for the new implementation of setoid_*).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6048 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23"Print Setoids" command added.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5968 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-18Abstraction vis a vis du type loc pour ocaml 3.08herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5951 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-08added commands to idecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5870 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-03but autoamtics tactics savingmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5723 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-30Achèvement du passage des emprunts à cameleon de Maxence Guesdon de la ↵herbelin
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
2004-04-13Ajout codingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5671 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-13Passage a la version 1.3 sous GPL des outils okey et configwin de cameleon ↵herbelin
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
2004-04-06warning dialog when save failsmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5641 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16mise a jour des menusmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5507 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15ajout des Print Scopes dans liste commandes sans effetmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5493 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-03ide: silent behavior better, save icon, -byte worksmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5427 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Localisation des erreurs d'internalisation des notations de tactiquesherbelin
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
2004-02-04bug fix find coqidecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5290 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-04highlightmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5289 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-04search windowcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5288 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29pour ide sous windowscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5267 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-20coqide utf8marche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5222 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-13Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables ↵herbelin
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
2004-01-02meilleure presentation des commentaires du traducteurbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-30ameliorations coqidecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5161 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-16coqide menus on golasmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5104 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-12plus de syntaxe v8marche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5089 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-09commandes de coqidemarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5081 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-08preferencesmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5077 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-08bug de preferencs/font"marche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5076 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-08pas de Goal pendant une preuvefilliatr
pas de Debug On/Off git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5075 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-05power associe a droitemarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5072 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-04changement menu et toolbarmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5065 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-01contrib jcfmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5053 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-28commands renomme en queries, command goto a la place de forward to backwardt omarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5015 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25textesmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4986 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-24aboutmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4983 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-24tentative de completion ESC-/ a la emacsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4981 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18.v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4943 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-03Check en plus parmi les keywordsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4785 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Conjecture declare maintenant un axiome; reorganisation VernacDefinitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4710 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Deplacement next_global_ident_away dans Termopsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4611 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 05:43:54 +0000