| Age | Commit message (Collapse) | Author |
|---|
|
coercion code for
simultaneous coercion of different arguments of an inductive type. Add tactics for dealing
with heterogeneous equality. Export more error reporting functions from Cases.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9886 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9879 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
l'unification sur les types (qui nécessite le coûteux hnf_constr pour
la compatibilité) que si le type contient encore des méta (et pour
cela on attend le dernier moment) ou si une coercion est
potentiellement à insérer.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9878 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
l'unification -r9842- avait introduit des appels inutiles et coûteux à
hnf_constr).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9875 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(cas d'un terme sans Rel libre), introduction au passage d'un nouveau
type d'evar EvarGoal pour raffinement du message d'erreur.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9868 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
métas permettant de savoir si une instance de méta vient d'un
with-binding ou d'une unification, et si elle a déjà été typée ou pas.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9866 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(en particulier, la décision de quelle instance garder quand une méta
a plusieurs solutions importe; comment trouver une critère objectif ?
la compatibilité demande à donner préférence aux instances trouvées
par with-bindings).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9855 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
métavariable est clos.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9854 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
d'unification des types des with-bindings en deux: les problèmes
d'unification susceptibles d'introduire une coercion sont retardés
(comme dans le commit r9850) et ceux susceptibles de fournir d'autres
instances restent faits au plus tôt (comme avant le commit r9850).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9851 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
apply afin de reculer au plus tard les décisions irréversibles et en
particulier de pouvoir typer les with-bindings modulo coercions :
- l'unification des types des métas données en with-bindings est
retardé à après l'unification (unify_0) de telle sorte que les
instances trouvées par unify_0 soient prioritaires et que la
décision d'insérer éventuellement des coercions autour des valeurs
données en with-bindings se fasse au dernier moment;
- toujours pour permettre d'insérer ultimement des coercions,
l'instantiation des with-bindings ne se fait plus
l'appel unify_0 (cf clenv_unique_resolver);
- pour permettre ce retardement sans limiter le test de conversion
que unify_0 fait sur les termes clos, on transmet à unify_0 les
métas données en with-bindings (ainsi l'instantiation de ces métas
peut être faite dynamiquement au moment du test de clôture);
- parce que les métas données en with-bindings qui sont en position
de rédex (cas d'un "apply f_equal with (f:=fun ...)" peuvent
simplifier le problème d'unification (et elles ne sont pas de
toutes façons pas réinférables au premier ordre), on continue à
les substituer avant l'appel à unify_0 (cf meta_reducible_instance);
- pour l'unification du second-ordre, on continue d'instancier les
with-bindings et d'unifier les types des with-bindings avant
unification;
- reste à régler un problème de compatibilité lorsque le résultat de
l'unification des types des with-bindings est utilisé pour rendre
un terme clos et pour permettre à unify_0 d'utiliser la conversion.
+ meilleure compatibilité de apply, split, left, right pour le code
qui l'utilise avec des bindings clos
+ nettoyage et uniformisation des clenv_match_args, clenv_missing, et assimilés
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9850 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
lemme n'est pas un lemme d'induction (plus précisément si la tête de
la conclusion n'est pas une variable), alors on n'instancie pas les
with-bindings pour que les unifications venant du filtrage de la
conclusion du lemme avec le but soient prioritaires (en effet
l'utilisation des types des with-bindings pour inférer des instances
-- portion du commit r9842 -- ne produit pas des solutions exactes
mais seulement des sous-types de solutions exactes alors que
l'unification avec le but produit des solutions exactes qui doivent
donc être considérées en priorité). Toutefois, dans certains cas, du
fait que unify_0 travaille modulo conversion uniquement sur les termes
clos, il faut quand même donner crédit aux instances données en
with-bindings pour que la conversion puisse être prise en compte et
ainsi retrouver un comportement au moins identique au précédent.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9847 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9843 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
de résoudre des buts comme celui-ci :
Record nat_retract : Type :=
{f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}.
Goal nat_retract.
exists (fun x => x) (fun x => x).
- Nouvelle tentative d'utilisation des types des metas/evars pour
inférer de nouvelles instances de metas/evars; permet par exemple
d'utiliser f_equal sans option with, mais aussi, avec la modif
précédente, de résoudre des buts tels que
Goal exists f:bool->Prop, f true = True.
exists (fun x => True).
[Les expériences passées avaient montré qu'en prenant en compte les
types dans l'unification, on peut unifier trop tôt une evars à une
mauvaise sorte; à défaut de mécanisme de prise en compte des problème
d'unification avec sous-typage, on s'est interdit ici d'unifier des
types qui sont des arités.]
- Tout les constr de tactic_expr deviennent des open_constr (même si seul
with_bindings les accepte au final... c'est pas l'idéal).
- Renommage env -> evd et templenv -> env dans clausenv.
- Renommage closed_generic_argument -> typed_generic_argument.
- Renommage closed_abstract_argument_type -> typed_abstract_argument_type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9842 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9831 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
details).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in",
"erewrite" et "erewrite in". Correction au passage des bugs #1461 et
#1522).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(les let-in étaient comptés comme des produits, introduisant une incohérence
sur le nombre de produits à instancier dans les lemmes appelés par apply).
- Export simplest_eapply pour utilisation dans Sophia/RecursiveDefinition.
- Doc développeur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9785 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
reduce_to_ind et reduce_to_ref a révélé que ceux-ci pouvaient contourner
l'opacité des constantes lorsque celles-ci apparaissaient comme argument
d'un match ou d'un fix (et ce depuis la V5.10 environ). Exemple:
Definition f (A B:Set) := pair A B. Opaque f.
Goal fst (f unit unit) -> True. intro H. destruct H. (* bypassed opacity *)
Definition f (A:Set) := A. Opaque f.
Goal (f unit) -> True. intro H. destruct H. (* didn't bypass opacity *)
Contourner le statut Opaque quand on recherche un inductif (ce qui est
le rôle de reduce_to_ind) ne paraît pas problématique (et il se trouve
d'ailleurs que CoRN/ftc/TaylorLemma.v en profitait). Ce contournement
de l'opacité a donc été généralisé au cas de constantes arrivant en
tête sans être argument d'un match ou d'un fix.
Contourner le statut Opaque quand on recherche une constante
particulière (ce qui est le rôle général de reduce_to_ref qui est
maintenant le seul à reposer sur one_step_reduce) paraît en revanche
plus douteux. Plus de contournement d'opacité pour reduce_to_ref donc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9768 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9761 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
fix/cofix avec réutilisation du nom de la constante dans les appels
récursifs), avec notamment uniformisation des comportements et des
noms de fonctions de réduction. En particulier, on a les changements
sémantiques suivants :
- léger changement de simpl: si appliqué à un fix explicite, il sait
réduire l'argument en un constructeur comme si le fix était caché
derrière une constante (cf exemple dans test-suite/output/reduction.v);
- léger changement de hnf: si appliqué à un match ou un fix explicite
et que l'argument de ce match ou de ce fix nécessite un calcul
impliquant des constantes récursives, il sait conserver les noms (à
la manière de simpl) comme il sait déjà le faire si ce match ou ce fix
était caché derrière une constante (cf exemple dans
test-suite/output/reduction.v);
- changement similaire de one_step_reduce utilisé dans reduce_to_*_ref
(difficile d'imaginer les effets mais sans doute très peu)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9760 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- le type val_kind n'embarque plus le constr (pb de cohérence avec
le context);
- en revanche, lors du calcul d'une valeur, on calcule aussi
l'ensemble des variables nommées dont la valeur peut dépendre;
- lors du clear_hyps, si la valeur dépend d'une variable effacée, on
invalide le calcul.
Corrige le bug #1419
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9733 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
obligations (even an opaque one).
Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes.
Various little subtac changes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9707 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
"R ?1 ... ?n <= T". Utilisation de cette fonction dans Setoid_replace au
au lieu de w_unify (suggestion de GG).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9673 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
+ petit nettoyage himsg.ml + petite uniformisation erreurs CannotUnify
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9668 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9664 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
variables, useful for debugging
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9652 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
fonctionner entre la V7.3 et la V8.0 (notation : "@ ?meta id1 ... idn")
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9644 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
la gestion des erreurs dans clear_hyps.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9571 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9560 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9536 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- ajouts des opérations clear_evar_hyps_in_evar,
clear_evar_hyps_in_constr et clear_evar_hyps dans Evarutil, qui
permettent de supprimer des hypothèses dans le contexte des evars,
en créant une nouvelle evar avec un contexte restreint;
- adaptation de clear_hyps dans Logic pour qu'elle mette à jour le
contexte des evars;
- adaptation de prim_refiner pour qu'elle renvoie le evar_map modifié;
- déplacement de la tactique Change_evars dans prim_rule.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9518 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
des tactiques (ne marchait que si l'instance était une application).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9516 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
comportement pré-inductifs polymorphes vis à vis du test d'inclusion
des hypothèses de section (i.e. test dans le noyau mais pas dans
typing.ml qui est le typeur utilisé généralement par les
tactiques). En effet, les variables de section sont vues par les
tactiques comme des variables locales qui sont modifiables (p.ex. par
conversion). Mais le changement de la signature des variables de
section fait échouer le typage noyau (qui exige une égalité syntaxique
des types de ces variables) pour les demandes de typage en provenance
des tactiques.
Quelle est la bonne solution ?
- Faut-il comparer les variables de section modulo réduction dans le noyau ?
- Faut-il continuer à utiliser un typeur qui ne teste pas les hyps de section
pour les tactiques, comme c'était le cas avant les inductifs polymorphes
(c'est la solution pragmatique adoptée pour résoudre #1325)
- Faut-il éviter la confusion entre variables de section et variables de but ?
Incidemment, branchement de Tacmach.hnf_type_of sur Retyping, ce qui,
outre des calculs de typage allégés pour les tactiques, évite aussi de
tomber sur le comportement du bug #1325.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9510 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9503 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9470 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(utilisation du nom de la contrainte de type)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9468 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9452 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
résoudre la clause with de apply/elim) sur la politique de renommage de
concrete_name
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9450 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
plus simples)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9446 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
uniformes dans le cas de types mutuellement inductifs)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9445 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Case15.v et CasesDep.v pas anormal)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9437 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
cas de création de nom par défaut; utilisation de _ comme nom dans evarutil.ml)
+ test régression bug #1041 + allègement syntaxe tactique evar
+ essai de ne pas faire dépendre les evars des variables anonymes afin
de résoudre le bug #932
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9433 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(un peu de doc de termops.mli au passage)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9424 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Benjamin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9406 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9399 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9392 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
degrés de liberté concernant les instances de méta (cumulativité et
possibilité d'éta-expansion) de telle sorte que la fusion d'équations
se fasse modulo ces degrés de liberté.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9389 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9388 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dans les définitions alors même que ce polymorphisme est débranché
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9336 85f007b7-540e-0410-9357-904b9bb8a0f7
|
