| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
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
|
|
is line, and those below, will be ignored--
M kernel/mod_subst.mli
M kernel/mod_typing.ml
M kernel/mod_subst.ml
M kernel/subtyping.ml
M kernel/modops.ml
M library/declaremods.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10849 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
account.
- Add test case for bug #1844 on Combined Scheme.
- Change Reflexive_partial_app_morphism to require a Reflexive proof to
cut down search earlier, without losing anything.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10846 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
par un appel à global_reference (ce qui évite au passage d'activer le
glob dumping).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10845 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Induction and Minimality schemes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10843 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
debugging and printing hint databases
- Typeclasses unfold now correctly adds _global_ unfold hints.
- New tactic autosimpl to do simplification using the declared unfold
hints in given hint databases.
- Work on auto-modulo-some-delta (the declared Unfold constants),
actually used mostly if the goal contains evars, as Hint_db.map_auto
does not work up-to any conversions (yet).
- Fix GenMul which was using the old semantics of failing early because
of variance checks, which is not possible in the new implementation.
- Restrict when reflexive_morphism may be used using an extern tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10842 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(~/.subversion/config n'avait pas la ligne magique
"* = svn:keywords=Author Date Id Revision" dans la section [auto-props]).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10841 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
de l'argument donné contient des métavariables (souhait
#1408). Beaucoup d'infrastructure autour des constantes pour cela mais
qu'on devrait pouvoir récupérer pour analyser plus finement le
comportement des constantes en général :
1- Pour insérer les coercions, on utilise une transformation
(expérimentale) de Metas vers Evars le temps d'appeler coercion.ml.
2- Pour la compatibilité, on s'interdit d'insérer une coercion entre
classes flexibles parce que sinon l'insertion de coercion peut prendre
précédence sur la résolution des evars ce qui peut changer les
comportements (comme dans la preuve de fmg_cs_inv dans CFields de CoRN).
3- Pour se souvenir rapidement de la nature flexible ou rigide du
symbole de tête d'une constante vis à vis de l'évaluation, on met en
place une table associant à chaque constante sa constante de tête (heads.ml)
4- Comme la table des constantes de tête a besoin de connaître
l'opacité des variables de section, la partie tables de declare.ml va
dans un nouveau decls.ml.
Au passage, simplification de coercion.ml, correction de petits bugs
(l'interface de Gset.fold n'était pas assez générale; specialize
cherchait à typer un terme dans un mauvais contexte d'evars [tactics.ml];
whd_betaiotazeta avait un argument env inutile [reduction.ml, inductive.ml])
et nettoyage (declare.ml, decl_kinds.ml, avec incidence sur class.ml,
classops.ml et autres ...; uniformisation noms tables dans autorewrite.ml).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10840 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
alias de module et l'application d'un foncteur.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10838 85f007b7-540e-0410-9357-904b9bb8a0f7
|
