aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Correction bug #1302Gravatar herbelin2007-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9494 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite au mail de Lionel a propos du Makefile: Gravatar letouzey2007-01-12
| | | | | | | | | | | | | | | | | 1) Disparition de test_extraction.v rebasculé dans test-suite/success/extraction.v Au passage, remplacement de quelques Set en Type pour ne pas avoir besoin du -impredicative-set. Et ajout de passes d'extraction en Haskell et Scheme. Simplification du Makefile en conséquence (plus de barestate) 2) Au passage, reparation (et embellissement) de extract_env. Depuis le passage de Claudio dans cette portion (il y a 2 ans ?), faire Extraction S (ou tout autre constructeur) echouait. Idem pour un nom d'inductif mutuel autre que le premier du paquet. Etonnant que personne n'ait remarqué ca plus tot... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9484 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction petits bugs du check de la test-suiteGravatar herbelin2006-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9466 85f007b7-540e-0410-9357-904b9bb8a0f7
* remplacement d'un test d'egalite par un test de convertibilite dans ↵Gravatar jforest2006-12-22
| | | | | | injection/discriminate/inversion pour corriger des bugs en presence de modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9459 85f007b7-540e-0410-9357-904b9bb8a0f7
* Alignement de la politique de renommage de rename_bound_var (utilisé pourGravatar herbelin2006-12-13
| | | | | | | | 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
* test condition de gardeGravatar barras2006-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9449 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dépliage du terme d'induction avant suppression quand celui-ci est unGravatar herbelin2006-12-13
| | | | | | | | terme arbitraire, possiblement dépendant, qui a été transformé en let-in (cf success/destruct.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9447 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur suppression des vars anonymes des contextes d'evars (echec ↵Gravatar herbelin2006-12-12
| | | | | | 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
* MAJGravatar herbelin2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9436 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test bug #932Gravatar herbelin2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9434 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
| | | | | | | | | | 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
* Raffinement de l'unification de "apply": mémorisation de certainsGravatar herbelin2006-11-19
| | | | | | | | | 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
* Corrige un bug de calcul du temps effectif cquand la dernière décimale est 0Gravatar herbelin2006-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9371 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction typoGravatar herbelin2006-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9369 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de dépliage de l'énoncé, si besoin est, dans apply inGravatar herbelin2006-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug refineGravatar herbelin2006-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9359 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug test complexitéGravatar herbelin2006-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9335 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout test setoid_rewrite (cf bug #1176); anglicisationGravatar herbelin2006-11-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9330 85f007b7-540e-0410-9357-904b9bb8a0f7
* Débranchement du polymorphisme de sorte sur les définitions dans TypeGravatar herbelin2006-10-30
| | | | | | | | | | | | (trop de problèmes à régler, comme par exemple des types identiques qui se retrouvent dans des sortes disjointes, résultant en davantage d'équations (eq Type(i) a b) et (eq Type(j) a b) avec i syntaxiquement distinct de j, que Coq ne sait en général pas traiter -- i.e. ne sait pas forcer i==j (cf contrib CatsInZF: échec du test "dependent" dans "rewrite"); autre problème: le ralentissement du prouveur (logic.ml)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9323 85f007b7-540e-0410-9357-904b9bb8a0f7
* missing Require LegacyRfieldGravatar barras2006-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9318 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
| | | | | | | | | 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
* Check that sort-polymorphic inductive types is not too laxGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9297 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cette dérivation de paradoxe passait en V8.1betaGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9294 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applatissement des noeuds application vide dans le filtrage Ltac (ex:Gravatar herbelin2006-10-25
| | | | | | | 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
* Test apply inGravatar herbelin2006-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9270 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le calcul de la classe dans class_args_of ne suivait pas celui de class_ofGravatar herbelin2006-10-21
| | | | | | | | (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
* Correction d'un vieux bug de coercion avec éta-expansion (utilisationGravatar herbelin2006-10-21
| | | | | | | 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
* Clarification des contraintes sur le contexte de paramètres desGravatar herbelin2006-10-17
| | | | | | | | | | | inductifs dans le test de sous-typage (exigence du même nombre d'arguments uniformes attendus mais pas d'exigence spéciale sur les définitions locales du contexte à partir du moment où les types et constructeurs sont convertibles quand généralisés par rapport au contexte de paramètres) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9247 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptation des tests suite à la modification de Rewrite .. in (r9201)Gravatar notin2006-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9239 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction test-suite suite à r9186Gravatar notin2006-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9238 85f007b7-540e-0410-9357-904b9bb8a0f7
* Exemple avec liaison des variables de filtrage du matchGravatar herbelin2006-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9228 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notations:Gravatar herbelin2006-10-09
| | | | | | | | | | | | - 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
* suite commit 9222 : rétablissement des tests autre que complexitéGravatar herbelin2006-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9224 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un répertoire de test de la complexitéGravatar herbelin2006-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9222 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de deux cas où les types inductifs n'étaient pas comparésGravatar herbelin2006-10-05
| | | | | | | | 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
* nouveau ring/fieldGravatar barras2006-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9197 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une passe sur l'injection et la discrimination...Gravatar herbelin2006-10-01
| | | | | | | | | | | | | | | | | | 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
* Corrections mineuresGravatar notin2006-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug de coercion de pattern introduit dans la 8.1betaGravatar herbelin2006-09-23
| | | | | | | | (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
* Correction bug #1179 (result of Notation.decompose_notation_key in wrong orderGravatar herbelin2006-09-23
| | | | | | | 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
* Wish #1187 granted (support for canonical structures that are recordsGravatar herbelin2006-09-23
| | | | | | | only up to some preliminary reductions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9166 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1229 (toplevel "unresolved evar" fled throughGravatar herbelin2006-09-23
| | | | | | | Declare Implicit Tactic support) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9165 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction filtrage des notations impliquant un "match" : la présenceGravatar herbelin2006-09-23
| | | | | | | | | | 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
* Test Tactic NotationGravatar herbelin2006-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9160 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de l'heuristique d'unification premier ordre flexible/rigideGravatar herbelin2006-09-15
| | | | | | | | | | | | 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
* Correction du bug #1181Gravatar jforest2006-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9138 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout unification pattern dans l'algorithme d'unification desGravatar herbelin2006-09-12
| | | | | | | 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
* Extension et réorganisation de l'interprétation des (co-)points fixesGravatar herbelin2006-09-01
| | | | | | | | | | | | | | | | | | | | | | - 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
* Diverses modifications autour de l'unification modulo conversion:Gravatar herbelin2006-08-28
| | | | | | | | | | | | | - 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
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
| | | | | | | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 03:08:54 +0000