| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-03-25 | Fully fixing bug #3491 (anomaly when building _rect scheme in the | Hugo Herbelin | |
| presence of let-ins and recursively non-uniform parameters). The bug was in the List.chop of Inductiveops.get_arity which was wrong in the presence of let-ins and recursively non-uniform parameters. The bug #3491 showed up because, in addition to have let-ins, it was wrongly detected as having recursively non-uniform parameters. Also added some comments in declarations.mli. | |||
| 2015-03-25 | Another example about the consequence of a wrong computation of the | Hugo Herbelin | |
| number of recursively uniform parameters in the presence of let-ins. In practice, more recursively non-uniform parameters were assumed and this was used especially for checking positivity of nested types, leading to refusing more nested types than necessary (see Inductive.v). | |||
| 2015-03-24 | Updating test-suite (see previous commit). | Hugo Herbelin | |
| 2015-03-24 | Fixing computation of non-recursively uniform arguments in the | Hugo Herbelin | |
| presence of let-ins. This fixes #3491. | |||
| 2015-03-24 | Fixing wrong rel_context in checking positivity condition. | Hugo Herbelin | |
| Parameters were missing in the context, apparently without negative effects because the context was used only for whd normalization of types, while reduction (in closure.ml) was resistant to unbound rels. See however next commit for an indirect effect on the wrong computation of non recursively uniform parameters producing an anomaly when computing _rect schemas. | |||
| 2015-03-22 | Qed export -> Qed exporting | Enrico Tassi | |
| 2015-03-13 | Add some tests for tryif | Jason Gross | |
| + adjusting for the removal of `admit` by Arnaud Spiwack. | |||
| 2015-03-11 | Fix regression in HoTT_coq_014.v | Enrico Tassi | |
| Admitted was not using the partial proof to infer discharged variables. Now it does. The fix makes no sense, but restore the old behavior. | |||
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi | |
| - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit | |||
| 2015-03-09 | Do not display the status of monomorphic constants unless in ↵ | Guillaume Melquiond | |
| universe-polymorphism mode. | |||
| 2015-03-08 | Test for bug #2951. | Pierre-Marie Pédrot | |
| 2015-03-07 | Test for #4035 (dependent destruction from Ltac). | Hugo Herbelin | |
| 2015-03-05 | Fix testsuite with respect to the new formatting of Fail messages. | Guillaume Melquiond | |
| 2015-03-03 | Fix test-suite file, this is open. | Matthieu Sozeau | |
| 2015-03-03 | Fix bug #3732: firstorder was using detyping to build existential | Matthieu Sozeau | |
| instances and forgeting about the evars and universes that could appear there... dirty hack gone, using the evar map properly and avoiding needless constructions/deconstructions of terms. | |||
| 2015-03-03 | Add missing test-suite files and update gitignore. | Matthieu Sozeau | |
| 2015-03-03 | Add a test-suite file ensuring coinductives with primitive projections | Matthieu Sozeau | |
| do not enjoy eta-conversion and do not allow the usual failure of subject reduction in presence of dependent pattern-matching. | |||
| 2015-03-03 | Fix test-suite file, this is currently a wontfix, but keep the | Matthieu Sozeau | |
| test-suite file for when we move to a better implementation. | |||
| 2015-03-03 | Fix bug #4103: forgot to allow unfolding projections of cofixpoints like | Matthieu Sozeau | |
| cases, in some cases. | |||
| 2015-03-03 | Fix bug #4101, noccur_evar's expand_projection can legitimately fail | Matthieu Sozeau | |
| when called from w_unify, so we protect it. | |||
| 2015-03-02 | Fix bug #4097. | Matthieu Sozeau | |
| 2015-02-27 | Adding a test for bug #3612. | Pierre-Marie Pédrot | |
| 2015-02-27 | Test for bug #3249. | Pierre-Marie Pédrot | |
| 2015-02-27 | Fix test for #3467, I had moved it in a dumb way. | Maxime Dénès | |
| 2015-02-27 | Add support so that the type of a match in an inductive type with let-in | Hugo Herbelin | |
| is reduced as if without let-in, when applied to arguments. This allows e.g. to have a head-betazeta-reduced goal in the following example. Inductive Foo : let X := Set in X := I : Foo. Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *) | |||
| 2015-02-27 | Fixing first part of bug #3210 (inference of pattern-matching return | Hugo Herbelin | |
| clause in the presence of let-ins in the arity of inductive type). | |||
| 2015-02-27 | Fix test for #3848, still open. | Maxime Dénès | |
| 2015-02-27 | Moving test for #3467 to closed after PMP's fix. | Maxime Dénès | |
| 2015-02-27 | Fix test-suite files for bugs #2456 and #3593, still open. | Maxime Dénès | |
| 2015-02-27 | Add test-suite file for #3649. | Maxime Dénès | |
| 2015-02-27 | Moving tests for #2456 and #3593 to "opened" until they're fixed. | Maxime Dénès | |
| 2015-02-27 | Made test for #3392 rely less on unification. | Maxime Dénès | |
| 2015-02-27 | Moving test of #3848 to "opened". | Maxime Dénès | |
| 2015-02-26 | Test for #2602, which seems now fixed. | Maxime Dénès | |
| 2015-02-26 | Test for bug #3298. | Pierre-Marie Pédrot | |
| 2015-02-26 | Fixing complexity tests for #4076. | Maxime Dénès | |
| 2015-02-26 | Revert "Fixing bug #4035 (support for dependent destruction within ltac code)." | Maxime Dénès | |
| This reverts commit 4e6c9891140932f452bb5ac8960d597b0b5fde1d, which was breaking compatibility because one could no longer use names of foralls in the goal without introducting them. Probably not good style, but it did break many existing developments including CompCert. Closes #4093 but reopens #4035. | |||
| 2015-02-26 | Moving test for bug #3681 as closed. | Pierre-Marie Pédrot | |
| 2015-02-25 | Another test for a variant of complexity problem #4076 (thanks to A. Mortberg). | Hugo Herbelin | |
| 2015-02-24 | Univs: Fix Check calling the kernel to retype in the wrong environment. | Matthieu Sozeau | |
| Fixes bug #4089. | |||
| 2015-02-23 | Compensating 6fd763431 on postponing subtyping evar-evar problems. | Hugo Herbelin | |
| Pushing pending problems had the side-effect of later solving them in the opposite order as they arrived, resulting on different complexity (see e.g. #4076). We now take care of pushing them in reverse order so that they are treated in the same order. | |||
| 2015-02-23 | Fix some typos in comments. | Guillaume Melquiond | |
| 2015-02-23 | Test for #3953 (subst in evar instances). | Hugo Herbelin | |
| 2015-02-23 | Fixing rewrite/subst when the subterm to rewrite is argument of an Evar. | Hugo Herbelin | |
| This was broken by the attempt to use the same algorithm for rewriting closed subterms than for rewriting subterms with evars: the algorithm to find subterms (w_unify_to_subterm) did not go through evars. But what to do when looking say, for a pattern "S ?n" in a goal "S ?x[a:=S ?y]"? Should we unify ?x[a:=S ?y] with ?n or consider ?x as rigid and look in the instance? If we adopt the first approach, then, what to do when looking for "S ?n" in a goal "?x[a:=S ?y]"? Failing? Looking in the instance? Is it normal that an evar behaves as a rigid constant when it cannot be unified with the pattern? | |||
| 2015-02-23 | Fixing occur-check which was too strong in unification.ml. | Hugo Herbelin | |
| 2015-02-23 | Fixing test #2830. | Pierre-Marie Pédrot | |
| 2015-02-23 | Fixing test for bug #3071. | Pierre-Marie Pédrot | |
| 2015-02-21 | Moving test for bug #3071. | Pierre-Marie Pédrot | |
| 2015-02-21 | Test for bug #4078. | Pierre-Marie Pédrot | |
| 2015-02-20 | A fix for #3993 (not fully applied term to destruct when eqn is given). | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite