aboutsummaryrefslogtreecommitdiff
path: root/test-suite/failure
AgeCommit message (Collapse)Author
2019-02-04Primitive integersMaxime Dénès
This work makes it possible to take advantage of a compact representation for integers in the entire system, as opposed to only in some reduction machines. It is useful for heavily computational applications, where even constructing terms is not possible without such a representation. Concretely, it replaces part of the retroknowledge machinery with a primitive construction for integers in terms, and introduces a kind of FFI which maps constants to operators (on integers). Properties of these operators are expressed as explicit axioms, whereas they were hidden in the retroknowledge-based approach. This has been presented at the Coq workshop and some Coq Working Groups, and has been used by various groups for STM trace checking, computational analysis, etc. Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr> Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2018-10-04test-suite: cleaningVincent Laporte
2018-10-04test-suite: rename a few filesVincent Laporte
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2018-03-09Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesMaxime Dénès
2018-03-08Fix SR breakage due to allowing fixpoints on non-rec valuesMatthieu Sozeau
We limit fixpoints to Finite inductive types, so that BiFinite inductives (non-recursive records) are excluded from fixpoint construction. This is a regression in the sense that e.g. fixpoints on unit records were allowed before. Primitive records with eta-conversion are included in the BiFinite types. Fix deprecation Fix error message, the inductive type needs to be recursive for fix to work
2018-02-27Update headers following #6543.Théo Zimmermann
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
2017-04-11Update various comments to use "template polymorphism"Gaetan Gilbert
Also remove obvious comments.
2016-03-25Test suite file for a bug in int31 arithmetic fixed a while ago.Maxime Dénès
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Fix test-suite fileMatthieu Sozeau
2015-06-24Extend test-suite for the positivity checker.Arnaud Spiwack
I wasn't very creative: I just added a single test by failure case in the positivity checker (plus one success). There should probably be tests with mutually inductives and co-inductives as well.
2015-01-12Update headers.Maxime Dénès
2014-07-22Add test-suite file for guard condition on cofixpoints.Maxime Dénès
2014-04-09Add another critical bug to the test-suite.Maxime Dénès
I have a fix, I'm reviewing it because there may be other bugs around.
2014-01-15Test case containing a proof of false due to a DeBruijn off-by-one error in theMaxime Dénès
code checking allowed sorts for elimination.
2013-12-21Test case for the buggy commutative cut subterm rule.Maxime Dénès
2013-12-17test guard condition against feature incompatible with prop-extBruno Barras
2013-12-17Tentative fix of the guardedness checker by Christine and me. All stdlib and ↵Matthieu Sozeau
test-suite pass.
2013-09-20Fix name clash in "failure/inductive.v".xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16800 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16799 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Merge "inductive?.v" tests into a single "inductive.v" test.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16798 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Use "Fail" rather than rely on exit code.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16792 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Uminus.v : prepare this test file for the use of Failletouzey
- Highlight the fact that the line defining "up" is the one which should fail. - Factor code with stdlib's Hurkens.v - This way, this test could become a "shouldnotfail" test by placing two final "Fail" (before the definitions of "up" and "paradox"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16791 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19universes-buraliforti-redef.v : repair a match after Pierre B. syntax changesletouzey
This file, which is currently expected to fail at the last line (with Universe Inconsistency), was actually failing earlier after Pierre Boutillier changed the patterns (parameters are required now). A final "Fail" will soon arrives here to avoid such issue in the future... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16790 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-18Unset Asymmetric Patternspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-05Fixing critical inductive polymorphism bug found by Bruno.herbelin
If two distinct parameters of the inductive type contributes to polymorphism, they must have distinct names, othewise an aliasing problem of the form "fun x x => max(x,x)" happens. Also insisted that a parameter contributes to universe polymorphism only if the corresponding occurrence of Type is not hidden behind a definition. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14511 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vherbelin
which did not test what it was supposed to test git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13970 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-23Fix inconsistency in Prop/Set conversion checkglondu
This commit fixes a bug that made the system inconsistent with proof irrelevance (the main idea being that Set = Prop by reflexivity). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13450 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-20Added examples for checking that the guard condition excludes subtermsherbelin
in impredicative types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13024 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-24Fixed bug #2260 (check of resolution of all evars in the declarationherbelin
of a lemma was no longer done). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12885 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
Implicit Arguments, Arguments Scope and Coercion fixed, noneffective Global in sections for Hints and Notation detected). Misc. improvements (comments + interpretation of Hint Constructors + dev printer for hint_db). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-08Fixed a bug introduced in revision 12265.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12378 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-08-11Relatively ad hoc fix to an ill-typed instantiation bug in typeherbelin
inference (see file failure/evar1.v) + fix of some CUMUL problems that were in the wrong direction. We assume for the fix that ill-typed unification problems come from subtyping where we don't know yet if a coercion has to be inserted or not, and hence are of the CUMUL form. More on suspending problems of the form ?n <= Type or Prop <= ?n has to be done yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12268 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-02fixed kernel bug (de Bruijn) + test-suitebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11646 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-27added tests for hyps reorderingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11635 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-04Évolutions diverses et variées.herbelin
- 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
2008-07-25Correction d'une incohérence de typage des inductifs polymorphes: lesherbelin
contraintes bornant par le haut le type de l'inductif (ce qui peut arriver quand l'inductif est argument d'une constante) étaient oubliées : on pouvait se retrouver avec des inductifs dont le type des constructeurs, une fois instancié par des paramètres) n'était plus typable (seul leur réduit, après expansion des constantes, était typable). [kernel, test-suite] + Affichage des inductifs (via Print) en prenant la forme utilisateur des constructeurs. + Correction warning dans compilation gallina.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11266 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-22fixed universes bug related to module inclusionbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10828 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-21test module include w.r.t. universe constraintsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10827 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-16Vérification que "rewrite in" se comporte comme "rewrite" et échoueherbelin
sans bêta-normaliser face à un bêta-rédex dont l'argument ne correspond pas à ce qui est à réécrire. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10224 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-29 15:39:33 +0000