| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9197 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Efficacité:
- remplacement du typage par du re-typage léger
- suppression d'un pf_nf suspect (cf bug #1173) [quid de la compatibilité ?]
- remplacement des tests aveugles de projection impossible par un
test qui vérifie au fur et à mesure que les filtrages sont autorisés
Réorganisation:
- factorisation des parties communes de injEq/discrEq/decompEq
(à noter l'ordre inverse de génération des équations dans inj et decomp...)
- uniformisation des noms "e" et "ee" utilisés dans la construction des
combinateurs de discrimination
Extension:
- ajout d'une clause "as" à injection
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9195 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9176 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
|
|
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
|
|
only up to some preliminary reductions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9166 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Declare Implicit Tactic support)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9165 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9160 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@9138 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
|
|
- Relâchement de l'exigence que les types des paramètres et le type
des (co-)points fixes soient donnés. Ils peuvent maintenant être
inférés à partir des autres informations de types.
- Plus de déclaration séparée de celles des fonctions d'un bloc de
points fixes qui n'interviennent pas dans la définition des autres
(collect_non_rec): remplacement par un simple warning en cas de non
dépendance mutuelle de toutes les fonctions du bloc (de toutes
façons les fonctions qui intervenaient dans les autres sans en
dépendre - càd les fonctions définissables avant la partie point
fixe - n'étaient pas détectées)
- Ajout du test de dépendance mutuel au cas des co-points fixes
Extension et réorganisation de l'interprétation des blocs de
définitions (co-)inductives: relâchement de l'exigence que les types
des paramètres soient donnés. Ils peuvent maintenant être inférés à
partir des autres informations des blocs d'inductifs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9108 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- extension de l'unification au cas de motifs (au sens de Dale Miller)
[appel de solve_pattern_eqn dans evar_conv_x],
- correction de bugs présumés dans real_clean et do_restrict_hyp
(prise en compte de la taille courante du contexte de de Bruijn),
- ajout d'une heuristique de beta-reduction de tete dans real_clean
(cf test-suite/success/unification.v),
- suppression de certains "try ... with _ => ...".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9088 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
InType) for "replace <c1> with <c2>" and "replace c1" and partially
for "autorewrite".
+ Adding a "by tactic" optional argument to "setoid_replace".
+ Fixing bug #1207
+ Add new test files for syntax change and updating doc.
+ Moving argument tactic extensions from extratactics to extraargs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9073 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
can be used outside the module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
famille
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9009 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
inductive
- bug correction in "Functional scheme" and "functional inversion": the
function are now parsed as references and not indent
- adding a zeta normalization function in rawtermops to zeta normalize
graph constructions (not used for now)
- Bug correction in generation of functional principle types (if an
arguments of the function has a type which is a sort)
- adding a new persistent table for functional induction informations
(graph,...)
- new save mechanism for functional induction principles (reuse of
proofs when possible)
- Minor bug correction in proof of principle.
- Distinguishing building_principles (that is save them) and making then
(just construct their proof term)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9000 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8998 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
des inductifs maintenant retourne des sortes d'inductives qui ne sont pas des variables) et test de non-régression
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8992 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
paramètres récursivement non uniformes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8987 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8986 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
fonctionne pas incorrectement
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8974 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
|
|
+ bug correction in proof of structural principles
+ up do to date test-suite/success/Funind.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8899 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8885 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8884 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8870 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8869 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8868 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8839 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8832 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
commit 7360 suite à mécompréhension du sens de isunit; ajout d'un test vérifiant l'absence de ce trou
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8811 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
|
|
unicode; ajout de nouvelles plages
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8800 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8792 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8761 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
'properties' de Subversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 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@8720 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8719 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
7833, et que la révision 8644 n'avait pas corrigé dans le bon sens;
renommage en mind_consnrealdecls pour éviter la confusion de sens
avec mind_nrealargs
- Correction de la description du type one_inductive_body
- Ajout test avec let-in dans params et dans type constructeur
(fichier Case12.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8653 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8127 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8113 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
assomption en cours de preuve.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8109 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8107 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7961 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
statut du paramètre de Acc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7921 85f007b7-540e-0410-9357-904b9bb8a0f7
|
