| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 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
|
|
de la conclusion du lemme
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9865 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
setoid_reflexivity may discover it is doing plain Leibniz stuff (see
exception Optimize in setoid_replace), and falls back to the usual
reflexivity. Except that this one, due to the lack of delta-red,
refuses to handle the job, and gives it back to setoid_reflexivity:
a loop is born.
quick fix for the moment: add some whd_betadeltaiota to reflexivity in
the special situation where reflexivity is called back by
setoid_reflexivity.
Similar issue & fix for symmetry, transitivity.
rewrite has potentially the same problem, but I can't manage to trigger
a wild loop in practice. This code clearly deserves a closer look
someday...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9852 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
|
|
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
|
|
apparaissant sans nom dans "refine" (quelques incompatibilités, par
exemple dans les preuves de Lannion/continuations/Nxaccu_ex.core_V1,
Bordeaux/Additions/log2_spec.ceiling_log2, et
Bordeaux/NewSearchTree/search_tree.rm).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9841 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
référence à des arguments génériques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9839 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9838 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9837 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9836 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
supportees
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9833 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(anomalie sur types non convertibles)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9830 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
details).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- correction du mode strict qui n'était pas si strict,
- option "Set Strong Strict Implicit" pour activer le mode strictement
strict (désactivé par défaut pour raison de compatibilité),
- option "Set Reversible Pattern Implicit" pour activer les implicites
inférables par unification-pattern (désactivé par défaut par compatibilité),
- option "Unset Printing Implicit Defensive" pour désactiver
l'affichage des implicites n'ayant pas été décelés stricts,
- option "Set Maximal Implicit Insertion" pour que les
applications soient saturées en implicites si possible,
- une optimisation du mode non strict pour que l'algo de
recherche des implicites renonce à calculer les occurrences non
strictes qui pourraient avoir à être affichées dans le mode défensif,
avec pour conséquence que le mode défensif, pour celui qui le veut,
devient a priori encore plus verbeux, ex:
Set Implicit Arguments.
Definition id x : nat := x.
Parameter f : forall n, id n = id n -> Prop.
Check (f (refl_equal O)).
(* Affichait: "f (refl_equal 0)" mais affiche maintenant
"f (n:=0) (refl_equal 0)" *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9812 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
par sa notation (p.ex. pour unfold ou pour lazy delta).
Ex: Goal 3+4 = 7. unfold "+".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9804 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9800 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9787 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9776 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9775 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
de la réduction paresseuse du lemme [eapply n'en profitait pas], et
l'un et l'autre profite de l'unification2nd ordre sur la forme réduite
du lemme [apply n'en profitait pas]).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9771 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9770 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
exemple de divergence soumis par Andrew Appel) [on renonce à
normaliser pour trouver l'ensemble minimal de variables liées dans le
2e membre d'une égalité dépendante]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9765 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
|
|
the form expr_0 ; [ expr_1 | ... | expr_n ] where expr_i could be empty, expr_i may be ".." or "expr ..". Note that "..." is a part of the metasyntax while ".." is a part of the object syntax. It may be necessary to enclose expr in parentheses. There may be at most one expr_i ending with "..". The number of expr_j not ending with ".." must be less than or equal to the number of subgoals generated by expr_0.
The idea is that if expr_i is "expr .." or "..", then the value of expr (or idtac in case "..") is applied to as many intermediate subgoals as necessary to make the number of tactics equal to the number of subgoals. More precisely, if expr_0 generates n subgoals then the command
expr_0; [expr_1 | ... | expr_i .. | ... | expr_m], where 1 <= i <= m, applies (the values of) expr_1, ..., expr_{i-1} to the first i - 1 subgoals, expr_i to the next n - m + 1 subgoals, and expr_{i+1}, ..., expr_m to the last m - i subgoals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9742 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
constr avec lequel on réécrit contient une hypothèse H, on ne réécrit
pas dans H (corrige le bug #1446)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9735 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9699 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
compile-verbose +
ajout Pp.strbrk pour faciliter les césures faciles + messages divers).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9666 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
d'occurrences (clause "at") dans ltac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9648 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9632 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
récupère toutes les exceptions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9628 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9600 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9582 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@9555 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9552 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9549 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9534 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9512 85f007b7-540e-0410-9357-904b9bb8a0f7
|
