| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
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
|
| |
|
|
|
|
|
|
|
| |
Amélioration affichage des univers. Réparation de petits oublis du premier
commit. Essai d'une nouvelle stratégie : si le type d'une constante
est mentionné explicitement, la constante est monomorphe dans Type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9314 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
(suppression au passage d'un cast dans constant_entry_of_com - ce
n'est pas normal qu'on force le type s'il n'est pas déjà présent mais
en même temps il semble que ce cast serve pour rafraîchir les univers
algébriques...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
None ne filtrait pas None à cause d'un PApp parasite)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9280 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9279 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
du rôle de l'argument (-1) de make_clenv_binding_apply; nouvelle
correction qui évite ce codage.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9277 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
Au passage, déplacement des tactiques cut and co plus en amont + commentaires.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9266 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
(avec comme conséquence des échecs en cas de beta-redex - cf coercions.v).
Allègements triviaux dans coercion.ml en passant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9257 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
de subst1 au lieu de subst_term). Indentation plus compacte au passage.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9255 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- prise en compte des variables liées non liées par la notation (bug #1186),
- test pour affichage des notations aussi sur les sous-ensembles
des lieurs multiples (cf notation "#" dans output/Notations.v),
- extension, correction et uniformisation de quelques fonctions sur
les constr_expr et cases_pattern (avec incidences sur rawterm.ml,
parsing et contrib/interface).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9226 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
réduction paresseuse.
Accessoirement, suppression d'un test evar_defined inutile car sur
résultat de whd_betadeltaiota qui contient la réduction evar de tête
dans coercion.ml; code mort du commit précédent dans pretyping.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9223 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9221 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
(remplacement de la normalisation complète des evars dans les termes
par une normalisation par nécessité - dans les types, c'est en général
des expressions plus petites)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9220 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
d'un constr c, on vérifie que c est clos dans l'environnement de m (#1183)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9217 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
vis à vis de l'équivalence engendrées par les modules non génératifs
(cf bug #1242)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9215 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9194 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
(les coercions ne marchaient plus quand le type du terme à filtrer
était connu). Ajout d'un test pour ce bug et pour le bug #1168.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9169 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
de paramètres réels du constructeur qui compte et non le nombre total
de paramètres de la coercion)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9168 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
only up to some preliminary reductions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9166 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
en dernière étape de la procédure d'unification
- Nouvelle fonction consider_remaining_unif_problems dédiée à la résolution
de l'unification premier ordre flexible/rigide
- Déplacement check_evars dans Evarutil
Question ouverte: que faire pour l'unif premier ordre flexible/semiflexible ?
(cf exemples d'application dans test-suite/success/evars.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9141 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9140 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
backtrack de eauto et le partage des evars entre buts, cela fait
davantage de choix irréversibles avec rupture de compatibilité.
Exemple:
but 1: |- P ?f
but 2: H1:a=b, H2:c=c, H3:g a = g b |- ?f a = ?f b
eauto sur le but 2 peut trouver au moins 3 solutions:
1- avec unif premier ordre, il peut trouver ?f=g, en appliquant exact H3
2- avec unif pattern, il peut trouver ?f=\_.c, en appliquant exact H2
3- en s'y prenant bien, il devrait pouvoir laisser ?f ouvert en appliquant
f_equal H1
Dans certains exemples (Orsay/FSets/PrecedenceGraph/PrecedenceGraph.v en
l'occurrence), ajouter l'unif pattern fait adopter la solution 2
plutôt que la solution 3. En attente d'un meilleur algorithme, abandon
donc de l'unif pattern des evars pour apply (ce qui n'empêche pas que,
déjà, la situation actuelle, qui utilise l'unif premier ordre, peut
conduire à faire des mauvais choix -- mais au moins on reste
compatible...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9134 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
passage de l'unification pattern au cas tant des Meta que des Evar.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9132 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
tactiques (unification.ml) + renommages (evarconv.ml) + exemple (unification.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9131 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9122 85f007b7-540e-0410-9357-904b9bb8a0f7
|
herbelin
msozeau
notin
jforest
bgregoir
corbinea