| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10910 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10909 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10908 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
the very handy Printf.ifprintf was not available on earlier ocaml.
This file now uses a very dirty compatibility hack.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10906 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10905 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
|
|
generation of NMake.v
- genN.ml becomes NMake_gen.ml
- no need to produce the corresponding binary: we use ocaml NMake_gen.ml > NMake.v
- beware! redoing a ./configure is mandatory after this commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10903 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
of NMake.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10902 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
coqinit.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10901 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
theories/Ints
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10900 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
For the moment, the Ints files are simply moved into directories in
theories/Numbers with meaningful names. No filenames changed, apart
from:
Zaux.v -> theories/Numbers/BigNumPrelude.v
MemoFn.v -> theories/Lists/StreamMemo.v
More to come...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10899 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10896 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
for debug / external output via coqtop.byte + Drop
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10895 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
+ un error qui devrait être un anomaly
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10893 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10892 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10891 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
notations work and bug #1846 gets completely fixed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10890 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
name after internalisation, to get the correct behavior with typeclass
binders. This simplifies the pretty printing and translation
of the recursive argument name in various places too. Use this
opportunity to factorize the different internalization and
interpretation functions of binders as well.
This definitely fixes part 2 of bug
#1846 and makes it possible to use fixpoint definitions with typeclass arguments in
program too, with an example given in EquivDec.
At the same time, one fix and one enhancement in Program:
- fix a de Bruijn bug in subtac_cases
- introduce locations of obligations and use them in case the obligation tactic
raises a failure when tried on a particular obligation, as suggested by
Sean Wilson.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10889 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
morphismes). Les mettre au niveau 90 est peut-être plus naturel mais
entraîne trop d'incompatibilités (cf commit 10813 et 10825)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10888 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10887 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10886 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
du filtrage. Cela permet de détecter les cas impossibles et de simuler
les contraintes d'inversion exprimables sous la forme d'un assignement
des arguments du constructeurs (cf le cas de Vtail dans Bvector.v).
Si l'on filtre sur t:I u1 .. un, et que chaque ui a la forme vi(wi)
avec vi composé uniquement de constructeurs, et que le résultat final
est P(w1,...,wn) (qui est éventuellement lui-même une evar) alors on
construit le prédicat
Q:=fun x1 .. xn y =>
match x1 .. xn y with
| v1(z) .. vn(z) t => P(z)
| _ .. _ _ => ?evar-speciale-cas-impossible
end
qui vérifiera bien que Q u1 .. un = P(w1,..,wp).
En raison de limitations de l'unification (on aurait besoin d'eta
conversion pour résoudre des problèmes du genre
"terme rigide == match x with _ => ?evar end", et besoin d'instanciation par
constructeurs pour des cas comme "A(y) = match ?evar with C x => A(x) end"),
je n'ai pas réussi à traiter le cas général.
Aussi, on adopte une stratégie pragmatique consistant à tester
plusieurs prédicats possibles :
- si un type final est donné, on essaie d'abord l'algorithme de
Matthieu et sinon le nouvel algorithme (permet par exemple de traiter
certains cas d'élimination dépendante de Bvector.v),
- s'il n'y a pas de type final, on essaie d'abord le nouvel algo et
sinon, on essaie avec un prédicat sans dépendance (permet de traiter
des cas compliqués comme celui de par cas sur I' dans le fichier
Case13.v de la test-suite).
Dans la pratique, il y a beaucoup de changement dans le code de compile_case.
- Par exemple, la compilation est maintenant toujours appelé avec un
prédicat (là où l'on pouvait avoir None, on a maintenant toujours au
moins une evar).
- En revanche, le membre droit des clauses est maintenant
optionnel. Si c'est None, c'est qu'on se trouve dans le cas d'une
branche impossible au moment du calcul du prédicat de retour.
- Aussi, on renonce aux PrLetIn et PrProd dans l'expression du
predicat de retour mais il faut savoir que c'est maintenant la liste
des tomatchs qui spécifie le contexte exact dans lequel le prédicat
de retour est bien typé.
- Et d'autres...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10883 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10882 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
rewrite interp_context to use this new code instead of doing
internalization by itself.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10881 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10880 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
in a separate function in Refiner and use it in eauto to capture the
same semantics as auto (which uses tclTRY) when trying tactics.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10879 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
particulier, TacCall(_,f,[]) est utilisé pour une référence à une
variable ltac ou une tactique et Reference(f) est utilisé pour une
référence à une variable ltac ou un constr (en passant,
standardisation de l'utilisation de constr: ou ltac: à setoid_ring).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10878 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
constantes qui avait été mise en place pour la 8.1gamma puis abandonné
pour cause entre autres d'inefficacité. Cette fois, on restreind le
polymorphisme au seul cas d'alias vers un inductif.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10877 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
bug "no level labelled 8" (camlp5 ne sait pas annuler un extend
lorsque le niveau initial existe mais est vide : l'appel à delete
efface le niveau au lieu d'annuler l'effet de extend et de revenir à
un niveau existant vide).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10876 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
delta conversion when it should (setoid_rewrite bug reported by
roconnor).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10874 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
LANG que si LC_ALL n'est pas lui-même défini)
--Cette ligne, et les suivantes ci-dessous, seront ignorées--
M Makefile.build
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10873 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
syntaxe interne de ring_lookup et field_lookup qui n'était pas assez
robuste pour supporter une syntaxe [ ... ] dans constr.
Déplacement de now_show de List.v vers Tactics.v, déplacement de "[ _ ]"
au niveau 0.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10872 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
n'étaient plus compilés depuis le 14 janvier 2004 (avant la 8.0), Why
ayant pris la suite de correctness.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10870 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
en présence de l'option -custom
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10869 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
in reasonable time), add (unfinished) documentation on type classes.
Put some classes into Prop explicitely as singleton inductive types are
no longer in Prop by default even if all the arguments are (is that
really what we want? roconnor says no).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10868 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10866 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10865 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
now. Fix proof scripts that failed correspondingly. Should make many
contribs compile again...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10863 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10862 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- pour le "try", la nouvelle erreur CannotFindWellTypedAbstraction
doit être catchable
- pour accomoder Type -1 dans le discharge, il faut un refresh_universes strict
- bugs dans les fichiers de test-suite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10861 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Un patch pour le bug de non vérification du typage de Stéphane L.
- Changement du fameux message "cannot solve a second-order matching problem"
en espérant, à défaut de savoir résoudre plus souvent le problème, que
le message est plus explicite.
- Divers changements cosmétiques.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10860 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(i.e. "Inductive unit := tt." conduisait à "t:Prop" alors que le
principe de la hiérarchie d'univers est d'être cumulative -- et que
Set en soit le niveau 0).
Une solution aurait été de poser Prop <= Set mais on adopte une autre
solution. Pour éviter le côté contre-intuitif d'avoir unit dans Type
et Prop <= Set, on garde la représentation de Prop au sein de la
hiérarchie prédicative sous la forme "Type (max ([],[])" (le niveau
sans aucune contrainte inférieure, appelons Type -1) et on adapte les
fonctions de sous-typage et de typage pour qu'elle prenne en compte la
règle Type -1 <= Prop (cf reduction.ml, reductionops.ml, et effets
incidents dans Termops.refresh_universes et Univ.super).
Petite uniformisation des noms d'univers et de sortes au passage
(univ.ml, univ.mli, term.ml, term.mli et les autres fichiers).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10859 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10858 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
fichiers en attendant une intégration à theories/Numbers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10857 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
des types des with-bindings dans la 8.1 [ceux-ci étaient déjà
utilisés et ce qui est vraiment nouveau est que l'unification est
maintenant celle de evarconv alors que c'était avant un mélange
d'unify_0 (sans delta) et de coercion sur les termes sans evars]. Je
renonce à maintenir la compatibilité (on se retrouve donc avec un
exemple qui fonctionne différement dans TermsConv.v de CoLoR).
- Robustesse accrue pour la nouvelle facilité de syntaxe de binding
avec paramètre pour pose/set.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10856 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
substitution. Makes unification succeed a bit more often, hence auto
works better in some cases.
- Backtrack the changes of auto using Hint Unfold to do more delta and add
a new tactic "new auto" which does that, for compatibility.
The first fix may have a big impact on the contribs, whereas the second
should make them compile again... we'll see.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10855 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
"pose as" de Program.
- Report des modifs de coercion.ml (révision 10840) dans subtac_coercion.ml.
- Comportement de "simple apply" rendu plus proche de celui du apply 8.1
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10854 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
failures in proof search. Catch Refiner.FailError in typeclasses eauto
to indicate that an extern tactic failed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10853 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
"set (f:=fun n => t)" (et idem pour pose).
Documentation notation Record sans sort et, en passant, "let|" -> "let '".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10852 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
setoid_rewrite, et dans Romega.
Pour info, ces fichiers ne sont pas compilés... (?)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10851 85f007b7-540e-0410-9357-904b9bb8a0f7
|
