| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11075 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11074 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
proof general (caractérisation des undos comme triplet d'un nombre de
Undo, n'un nombre de Abort et d'un Reset vers un état/id).
C'est plus simple et cela permet en plus d'avoir des buts imbriqués.
Au passage, "goto point" se comporte comme une suite de "one step back".
- Quelques bricoles sur la fenêtre préférences de Shortcuts.
- Quelques réorganisations autour du menu Display.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11058 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11044 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11042 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- typo du configure;
- warnings variables non utilisées dans ide/utils;
- suppression des variables vides COQINSTALLPREFIX et OLDROOT parce
que l'option -e que l'on aurait pu en principe utiliser pour les
surcharger ne fonctionne pas lorsqu'il y a plusieurs niveaux
d'imbrication de makefiles (comme c'est le cas quand on vient
du makefile servant à faire les packages qui appelle le makefile
principal qui appelle les makefile.stage);
- utilisation de ALLVO plutôt qu'un find pour trouver les .v sur
lesquels appliquer coqdep (permet d'éviter des warning sur les fichiers
de test, non prévus pour faire partie de la biblio standard);
- utilisation de -custom sur les bytecode qui ne l'étaient pas encore
(coqchk et coqmktop) pour être indépendant de ocamlrun à
l'installation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11029 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11018 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11011 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11009 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
coq (mais ça ne rend pas très bien -- faudrait centrer l'image)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11007 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
|
|
- Divers code mort (evarutil.ml, Bvector.v)
- MAJ perf-analysis
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11004 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
are no useless in coqide
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10994 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
with shortcuts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10992 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10990 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10989 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10985 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
l'affichage des instances des evars.
- Nouveaux boutons "interrupteurs" pour activer/désactiver à volonté
l'affichage des implicites, coercions, notations, etc dans CoqIDE
(reste à trouver des icônes appropriées !).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10983 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
améliorer l'efficacité du undo. Restent les Qed et les End dont le
undo peut nécessiter de rejouer un segment arbitrairement complexe
(pour le undo du Qed, il faudrait typiquement que Coq se souvienne
de l'entrelacement de déclarations et de tactiques).
- Code mort concernant les mots-clés dans coq.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10982 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10958 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
à potentiellement modifié l'état, on ne peut se contenter d'un Abort :
il faut revenir au dernier état connu).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10951 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10950 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
complexité exponentielle dans la machine lazy depuis que l'algo de
compilation du filtrage évite systématiquement d'expanser quand le
filtrage n'est pas dépendant.
- Un peu plus de colorisation dans coqide.
- Utilisation de formats pour améliorer de l'affichage des notations Utf8.
- Systématisation paire Local/Global dans g_vernac.ml4 (même si le
défaut n'est pas toujours le même)
- Bug Makefile
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10918 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
|
|
des théorèmes prouvés par récursion ou corécursion mutuelle.
Correction au passage du parsing et du printing des tactiques
fix/cofix et documentation de ces tactiques.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10709 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10619 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
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
|
|
devient Flags.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10236 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10230 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10229 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10219 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10199 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10175 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10113 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
