aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/destruct.v
AgeCommit message (Collapse)Author
2009-10-04Removal of trailing spaces.serpyc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12371 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-27Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12359 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-27Delay the choice of eliminator in destruct/induction until we know ifherbelin
a dependent scheme is needed or not (this allows for instance "destruct H" when H is propositional and dependent in the context to work). Modest attempt to clarify the basic components used and invariants preserved when sharing the code for functional induction and for destruct/induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12356 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-23Add support for dependent "destruct" over terms in dependent types.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11944 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-18Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkherbelin
(résolution entre autres des bugs 1882, 1883, 1884). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11145 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
- vérification de la cohérence des ident pour éviter une option -R avec des noms non parsables (la vérification est faite dans id_of_string ce qui est très exigeant; faudrait-il une solution plus souple ?) - correction message d'erreur inapproprié dans le apply qui descend dans les conjonctions - nettoyage autour de l'échec en présence de métas dans le prim_refiner - nouveau message d'erreur quand des variables ne peuvent être instanciées - quelques simplifications et davantage de robustesse dans inversion - factorisation du code de constructor and co avec celui de econstructor and co Documentation des tactiques - edestruct/einduction/ecase/eelim et nouveautés apply - nouvelle sémantique des intropatterns disjonctifs et documentation des pattern -> et <- - relecture de certaines parties du chapitre tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-13Dépliage du terme d'induction avant suppression quand celui-ci est unherbelin
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
2006-05-31Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la casseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8884 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02commentaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5789 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-20Protection du destruct pour vérifier que ce n'est pas une anomalie, à ↵herbelin
défaut de faire réussir la tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5754 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-02Ajout test bug 711herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5720 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 00:43:09 +0000