| Age | Commit message (Collapse) | Author |
|---|
|
coercion to funclass) [added a new notation output test as the
initial one is quite saturated in miscellaneous notations].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11886 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11805 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
late 2008 Coq WG.
- Updated Copyright file wrt JProver.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11781 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11740 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11736 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Fixed a virtual bug of unification (ever occurs if w_unify called with
a non-empty context of rel's, which is a priori uncommon).
- Fixed Notation.out test.
- Add better coqide error message in case editor is called on an unnamed file.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11650 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11641 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Ajout test pour non-régression du bug #1968
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11569 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Correction bug #1815 sur "coqide dir_inexistant/nom_fichier"
- Tests oubliés de la révision 11438 (amélioration affichage coercions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11555 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
entre le calcul des arguments récursifs possibles -- bien que bidon en
attendant mieux -- et ce la tactique fix attend -- le premier expanse
les produits au maximum le second non)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Fixed doc of assert as.
- Doc of apply in + update credits.
- Nettoyage partiel de Even.v en utilisant "Theorem with".
- Added check that name is not in use for "generalize as".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11511 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Prise en compte des notations applicatives
- Remplacement du codage des arguments liste des notations récursives
sous forme de terme par une représentation directe (permet notamment
de résoudre un problème de stack overflow de la fonction d'affichage)
+ Correction bug affichage Lemma dans ppvernac.ml
+ Divers util.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11489 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- evarconv: mauvaise idée d'utiliser la conversion sur la tête d'un
terme applicatif au moment de tester f u1 .. un = g v1 .. vn au
premier ordre : on revient sur l'algo tel qu'il était avant le
commit 11187.
- Bug #1887 (format récursif cassé à cause de la vérification des idents).
- Nouveau choix de formattage du message "Tactic Failure".
- Nettoyage vocabulaire "match context" -> "match goal" au passage.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11305 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Correction divers messages d'erreur
- lorsque rien à réécrire dans une hyp,
- lorsqu'une variable ltac n'est pas liée,
- correction anomalie en présence de ?id dans le "as" de induction,
- correction mauvais env dans message d'erreur de unify_0.
- Diverses extensions et améliorations
- "specialize" :
- extension au cas (fun x1 ... xn => H u1 ... un),
- renommage au même endroit.
- "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize".
- "induction"
- intro des IH toujours au sommet même si induction sur var quantifiée,
- ajout d'un hack pour la reconnaissance de schémas inductifs comme
N_ind_double mais il reste du boulot pour reconnaître (et/ou
réordonner) les composantes d'un schéma dont les hypothèses ne sont pas
dans l'ordre standard,
- vérification de longueur et éventuelle complétion des
intropatterns dans le cas de sous-patterns destructifs dans induction
(par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas
le n dans le contexte),
- localisation des erreurs d'intropattern,
- ajout d'un pattern optionnel après "as" pour forcer une égalité et la
nommer (*).
- "apply" accepte plusieurs arguments séparés par des virgules (*).
- Plus de robustesse pour clear en présence d'evars.
- Amélioration affichage TacFun dans Print Ltac.
- Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu
(incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !).
- Fusion VTactic/VFun dans l'espoir.
- Mise en place d'un système de trace de la pile des appels Ltac (tout en
préservant certains aspects de la récursivité terminale - cf bug #468).
- Tactiques primitives
- ajout de "move before" dans les tactiques primitives et ajout des
syntaxes move before et move dependent au niveau utilisateur (*),
- internal_cut peuvent faire du remplacement de nom d'hypothèse existant,
- suppression de Intro_replacing et du code sous-traitant
- Nettoyage
- Suppression cible et fichiers minicoq non portés depuis longtemps.
(*) Extensions de syntaxe qu'il pourrait être opportun de discuter
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11296 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11294 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Correction au passage d'un bug de Arguments Scope Global
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11199 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
nom dans l'état initial)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11053 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
|
|
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
|
|
test-suite/output/ZSyntax.out
typo
test-suite/bugs/closed/shouldsucceed/1776.v
bug closed
test-suite/success/extraction.v
test-suite/success/extraction.v
test-suite/bugs/closed/shouldsucceed/846.v
backtrack sur le commit 10639
test-suite/bugs/closed/shouldsucceed/1322.v:
petites modifications suite aux changement de setoid_replace
test-suite/bugs/closed/shouldsucceed/1414.v:
petites modifications suite aux changement dans Program
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10723 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
engendrees par les alias de module
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
implementation. Mostly syntax changes when declaring parametric
relations, but also some declarations were relying on "default"
relations on some carrier. Added a new DefaultRelation type class that
allows to do that, falling back to the last declared Equivalence
relation by default. This will be bound to Add Relation in the next
commit.
Also, move the "left" and "right" notations in Program.Utils to "in_left" and
"in_right" to avoid clashes with existing scripts.
Minor change to record to allow choosing the name of the argument for
the record in projections to avoid possible incompatibilities.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10639 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
kernel:
-declaration.ml
unification des representations pour les modules et modules types.
(type struct_expr_body)
-mod_typing.ml
le typage des modules est separe de l'evaluation des modules
-modops.ml
nouvelle fonction qui pour toutes expressions de structure calcule
sa forme evaluee.(eval_struct)
-safe_typing.ml
ajout du support du nouvel operateur Include.(add_include).
library:
-declaremods.ml
nouveaux objets Include et Module-alias et gestion de la resolution de noms pour
les alias via la nametab.
parsing:
-g_vernac.ml4:
nouvelles regles pour le support des Includes et pour l'application des signatures
fonctorielles.
extraction:
Adaptation a la nouvelle representation des modules et support de l'operateur with.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10497 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10462 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
filtrage; sauts de line intempestifs dans pretty.ml)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10179 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
the latter is bound to a var which is not a quantified one - this led
to remove a line marked "temporary compatibility" ... ; made a distinction
between quantified hypothesis as for "intros until" and binding names as
in "apply with"; in both cases, we now expect that a identifier not used
as a variable, as in "apply f_equal with f:=g" where "f" is a true binder
name in f_equal, must not be used as a variable elsewhere [see
corresponding change in Ints/Tactic.v])
- Fixing bug 1643 (bug in the algorithm used to possibly reuse a
global name in the recursive calls of a coinductive term)
- Fixing bug 1699 (bug in contracting nested patterns at printing time
when the return clause of the subpatterns is dependent)
- Fixing bug 1697 (bug in the TacAssert clause of Tacinterp.subst_tactic)
- Fixing bug 1678 (bug in converting constr_pattern to constr in Constrextern)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10131 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10040 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9988 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
@nil".
Ajout @ref au niveau constr pour allègement syntaxe.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9819 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
discussion avec Georges)
- La notion d'insertion maximale n'est plus globale mais attachée à
chaque implicite
- Correction de petits bugs dans le calcul des implicites
- Raffinement de la notion "sous contexte" pour l'affichage des coercions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9817 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9436 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9238 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9228 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9176 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
leading to wrong/failing printing of notations such as "- 1" or "1 -").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9167 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
des localisations empêchait toute unification des pattern de filtrage
de réussir.
- Ajout au passage d'unification des pattern modulo alpha.
- Exemples dans Notations.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9163 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
d'éviter l'affichage de trop d'espacements dans Tactics et de prendre une décision sur le rôle du _ dans Cases
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8935 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8870 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
un module
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8801 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
PCase dans le type pattern: le type pattern est utilisé
essentiellement dans ltac, il est normalement obtenu sans typage, et
ce via rawconstr (sauf cas de filtrage ltac non linéaire où il est
obtenu de constr). Le cas d'un filtrage sur un "if" doit être traité à
part car sans le type, il est impossible de savoir le nombre
d'arguments du constructeur puisque par définition du "if", ceux-ci ne
sont pas liants et ne laissent pas dans la syntaxe concrète
(résolution au passage du bug #1070, dû à un filtrage incomplet dans
le passage de pattern à rawconstr permettant l'affichage des pattern).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8728 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7847 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7798 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7774 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7707 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7704 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7701 85f007b7-540e-0410-9357-904b9bb8a0f7
|
