aboutsummaryrefslogtreecommitdiff
path: root/ide
AgeCommit message (Collapse)Author
2008-03-30Modifications diverses et variées :herbelin
- Nouvel essai de prise en compte unfold dans apply (unification.ml) - Correction bug commit précédent (constrintern.ml) - Correction bug d'explication des evars non résolues (evarutil.ml) - Fenêtre de query coqide plus large (command_windows.ml) - Orthographe tauto (tauto.ml4) - Crédits (ConstructiveEpsilon.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10731 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-23CoqIDE default font set to monospace so as indentation to be meaningfulherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10709 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-04Branchement de l'auto-save de coqide par défautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10619 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-10Correction du bug #1770: il semble que la recherche insensible à la casse ↵notin
ne soit pas implantée (cf backward-search et forward-search dans GText.iter et Gtk.Tags.text_search_flag) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10435 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-13migration of ide/utf8.v to theories/Unicode/Utf8.vletouzey
These notations aren't CoqIDE-specific, I can now use them with ProofGeneral (after a small modification of PG, contact me if you're interested by the patch). So let's place this file in a globally visible subdir of theories/. By the way, the filename is now uppercase as all other .v files. By the way, minor other changes in Makefile : extraction/test doesn't exist anymore, and tags / otags can be made without re-doing any find. NB: be sure to use etags that comes from emacs and not the one of exuberant-ctags, since the latter has now a different syntax (in debian, see update-alternatives etags). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10376 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-06Commit intermédiaire express de réparation de coqide.ml, que j'avais aspiwack
tout cassé hier sans m'en rendre compte (le soucis de travailler sur un ordinateur où j'ai pas installé lablgtk2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10347 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting des fonctions (à un ou deux arguments tous ou partie de type option). Il reste quelques opérations dans Util à propos desquelles je ne suis pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain car il est tard (comme some_in qui devrait devenir Option.make je suppose) . Elles s'expriment souvent facilement en fonction des autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y" . Le option_cons devrait faire son chemin dans le module parce qu'il est assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml. J'en ai profité aussi pour remplacer les trop nombreux "failwith" par des erreurs locales au module, donc plus robustes. J'ai trouvé aussi une fonction qui était définie deux fois, et une définie dans un module particulier. Mon seul bémol (mais facile à traiter) c'est la proximité entre le nom de module Option et l'ancien Options. J'ai pas de meilleure idée de nom à l'heure qu'il est, ni pour l'un, ni pour l'autre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-18Report de la révision #10197 (adaptation à Lablgtk 2.10.0)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10236 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-16add visibility of extraction messages in coqideletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10230 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-16Correction d'un bug de l'appel à make via Coqidenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10229 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-12Maj du lien vers coq-bugs dans Coqidenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10219 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-09Amélioration de l'appel aux outils externes via Coqidenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10199 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-04 Bug 1716: Scheme now print the right messagesvsiles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10175 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-04fixed iconsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10113 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-26fin des conclusions multiplescorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-25New keyword "Inline" for Parameters and Axioms for automatic soubiran
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
2007-04-16Add the possibility to change the position of tabs in main window (from r9717).glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9774 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-16Fix a bug which sometimes made coqide crash after changingglondu
preferences (first fixed in rev. 9716). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9773 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-16Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9656 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-31redirection of errors in coqide + dynamic warning printer (needed for tm_egg)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9566 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-25decl mode: anonymous factscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9534 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-12addition du neq unicodeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9482 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-07Changement des modifeurs par défaut dans CoqIDE (problème de ↵notin
compatibilité entre architecture) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9349 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28Suite commit 9256: autres cas incorrects de prise en compte de @ dans les identherbelin
pour F4 dans CoqIDE git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9307 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-23fixed same_file (#1141)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9263 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-23fixed non-bug #1213barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9262 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-21Pas d'@ dans les identificateurs (pour F4 and co)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9256 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-19coqide: affichage des sous-buts et hypothèses et métas comme types deherbelin
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
2006-10-13Ajout des options Coqide suggérées par Damien Doligez (wish #1053)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9240 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-29Suppression des warnings à la compilationnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9189 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-20Declarative Proof Language: main commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Suite commit 9110 (uniformisation position notation dans les blocs inductifs)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9113 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-28Modifications dans les scripts de configuration (coqtop et coqide affichent ↵notin
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
2006-07-06Remplacement VernacDebug par VernacSetOption (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9024 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Ajout d'une option -with-geoproof à la configuration et à l'exécutionnotin
pour inhiber la gestion de Geoproof sous Coqide (qui peut poser des problèmes avec GTK < 2.6.0) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8932 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Correction du bug #728(1086) (ordre de sauvegarde des tactiques dans coqide)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8920 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07Changement de l'option -where: on vérifie si la variable d'environnement ↵notin
COQLIB est définie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8912 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-31Colorisation dans Coqidenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8880 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-30Correction bug #990 (LoadPath et option -R de coqidenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8877 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-02Affichage des warning gtk comme warning coqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8776 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵notin
'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Standardisation nom option_app en option_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-08 r8623@thot: notin | 2006-03-08 12:40:57 +0100notin
Passage à la version LGPL de Configwin dans le trunk git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8618 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
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
2006-01-05*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7803 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-13changing the name of drgeocaml into GeoProofnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7644 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-26coqide send a ack to tell drgeocaml it is receivednarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7614 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-25*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7609 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-25*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7608 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 19:28:30 +0000