| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In trunk: New strategy for compiling and finding index_url.txt. After
all, this file is not specific to CoqIDE but to the
documentation. Hence, it seems better to install it close to the
documentation. If the documentation is locally installed, it is easy
to find the file index_url.txt but what to do if the documentation is
remote? We would need a http getter. Does this mean we have to rely on
wget or so? In the absence of answer to this question, it seems
reasonable, first to assume the doc to be locally installed, second to
have a local copy of index_url.txt ready in the installation directory
of CoqIDE.
Also added an "automatic" field in the CoqIDE url preference to
prevent the user to have to update his preference file every time a
new version of Coq is out and the link to the doc change.
In 8.2: Added a minima the installation of index_urls.txt but the user
will have to update its preferences because the links
"http://coq.inria.fr/doc/Reference-Manual010.html#..." do not longer
exist.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12278 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- removed circular dependency between record and class used to keep
track of sessions => no need for mutable option in record.
- more 'a option ref pruning
- more code splitting
- more alpha-rewriting
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11968 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
principaux changements sont:
- coqtop (et coqc) maintenant insensible aux variables
d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les
librairies Coq peut être spécifié par l'option -coqlib
- coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et
-camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les
chemins des exécutables OCaml; en dehors du mode boot, coqmktop
cherche les exécutables OCaml dans PATH
- installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci
étant installé en copiant l'architecture des sources (ie lib.cmxa
est installé dans COQLIB/lib/lib.cmxa)
- coq_makefile prend maintenant 3 paramètres sous forme de variables
d'environnement: COQBIN pour dire où trouver les exécutables Coq,
CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les
chemins vers les librairies sont déduits en utilisant -where
Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de
simuler les conditions de la vie réelle (Ocaml pas dans le PATH,
installation binaire relocalisée, ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11093 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
n'étaient pas gérés, merci à Julien).
- Correction pb blocage CoqIDE quand le browser n'est pas déja lancé
(utilisation pour cela de Sys.command au lieu de Unix.open_process_full).
- MAJ CHANGES et COMPATIBILITY.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11022 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11019 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
save as dialogs of coqide to a not deprecated widget, add filtering of *.v files in these dialogs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11006 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
commit 10916
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10917 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Colorisation:
- on ne colorie que les noms de commandes que si en début de phrase
(par exemple: Definition F := fun Local => Local) ne colorie pas
Local),
- ajout de motifs plus sophistiqué, (par exemple, tous les Set/Unset
sont uniformément mis en valeur).
- Backtracking: résolution bug #1538 et réactivation de la possibilité de
déclarer des défs, types, etc pendant une session de preuve. En revanche,
il n'est pas clair que cela fonctionne bien avec le mode déclaratif.
- Messages d'erreur : on ne capture la sortie de coq qu'après
l'initialisation pour que les erreurs d'initialisation soit
affichées (cf bug #1424 and item 5 of #1123).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10915 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Suppression d'une source de fuite mémoire dans declare_mod.ml (la
table de hash library_table n'était pas synchronisée avec le reset
et elle grossissait à chaque rejeu de la session; utilisation au
passage d'une map pour que la synchronisation avec le reset soit
plus rapide). [mod_typing.ml]
- Correction d'un bug de synchronisation pour le niveau pattern 200.
[pcoq.ml4]
- Suppression d'un vieux reste du traducteur [constructeur VernacVar]
- Robustesse et uniformité accrue dans CoqIDE vis à vis du statut de
chacune des commandes vernaculaires par l'utilisation d'une fonction
d'assignation d'attributs à chaque commande vernac.
Correction de ce qui semble être des bizarreries
(VernacDeclareTacticDefinition considéré comme ouvrant un but;
suppression des "loc" dans les Reset: ne pouvait pas faire
fonctionner correctement update_on_end_of_segment).
Suppression de la nécessité d'expliciter si une commande retourne
des messages dépendants du mode "verbose" (on suppose que chaque
commande sait ce qu'elle doit dire selon la position du flag verbose).
Sinon, le mécanisme de Reset de CoqIDE reste pauvre. CoqIDE ne
sait revenir qu'aux états associés à des noms et cela ne vaut pas
l'approche de Proof General. Il sera sans doute opportun de se
brancher sur l'architecture de Pierre Courtieu à base de "Backtrack".
La restriction des buts imbriqués a-t-elle vraiment une raison
d'être ? En plus les commandes non cablées en dur comme Next
Obligation ne sont pas prises en compte.
Interdiction, dès Coq, d'ouvrir sections ou modules si preuve en cours.
Réparation approximative de l'option "Help for Keyword" de Coqide
mais encore à faire pour plus de robustesse (makefile, installation,
synchronisation entre la version du fichier index_urls.txt et la
version du refman, ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10904 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
devient Flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9566 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9263 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
COQLIB est définie
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8912 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7609 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7608 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7603 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
ocaml 3.09
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7041 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5288 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5267 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5161 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4424 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4232 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4221 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4155 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4059 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4040 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4021 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3963 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3949 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3947 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3787 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3756 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
autorepeat des paste. configuration des accel rateurs. les chaines peuvent contenir des points. Bug: les phrases ne peuvent pas contenir .\sep. Or c'est permis par les Notation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3750 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3747 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3741 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3736 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3734 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3729 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3725 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3724 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Contextual colorization. Synchronization problems solved.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3719 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
properly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3705 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3700 85f007b7-540e-0410-9357-904b9bb8a0f7
|
