Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge branch 'v8.5' | 2015-04-15 | |
|\ | |||
| * | Test for bug #3199. | 2015-04-10 | |
| | | |||
| * | Better test-suite files, removing reliance on admit. | 2015-04-09 | |
| | | |||
| * | Fix declarations of instances to perform restriction of universe | 2015-04-09 | |
| | | | | | | | | instances as definitions and lemmas do (fixes bug# 4121). | ||
| * | Add test-suite file for bug #4120. | 2015-04-09 | |
| | | |||
* | | Merge branch 'v8.5' into trunk | 2015-04-09 | |
|\| | |||
| * | Test for bug #3815. | 2015-04-06 | |
| | | |||
| * | Fixing test-suite. | 2015-03-31 | |
| | | |||
* | | Merge branch 'v8.5' into trunk | 2015-03-30 | |
|\| | |||
| * | Adding test for bug #4165. | 2015-03-29 | |
| | | |||
| * | Updating test-suite (see previous commit). | 2015-03-24 | |
| | | |||
| * | Fixing computation of non-recursively uniform arguments in the | 2015-03-24 | |
| | | | | | | | | presence of let-ins. This fixes #3491. | ||
* | | Merge branch 'v8.5' into trunk | 2015-03-13 | |
|\| | |||
| * | Fix regression in HoTT_coq_014.v | 2015-03-11 | |
| | | | | | | | | | | Admitted was not using the partial proof to infer discharged variables. Now it does. The fix makes no sense, but restore the old behavior. | ||
* | | Merge branch 'v8.5' | 2015-03-11 | |
|\| | |||
| * | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | 2015-03-11 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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 | ||
| * | Test for bug #2951. | 2015-03-08 | |
| | | |||
| * | Test for #4035 (dependent destruction from Ltac). | 2015-03-07 | |
| | | |||
* | | Merge branch 'v8.5' | 2015-03-04 | |
|\| | |||
| * | Fix test-suite file, this is open. | 2015-03-03 | |
| | | |||
| * | Fix bug #3732: firstorder was using detyping to build existential | 2015-03-03 | |
| | | | | | | | | | | | | 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. | ||
| * | Add missing test-suite files and update gitignore. | 2015-03-03 | |
| | | |||
| * | Fix test-suite file, this is currently a wontfix, but keep the | 2015-03-03 | |
| | | | | | | | | test-suite file for when we move to a better implementation. | ||
| * | Fix bug #4103: forgot to allow unfolding projections of cofixpoints like | 2015-03-03 | |
| | | | | | | | | cases, in some cases. | ||
| * | Fix bug #4101, noccur_evar's expand_projection can legitimately fail | 2015-03-03 | |
| | | | | | | | | when called from w_unify, so we protect it. | ||
| * | Fix bug #4097. | 2015-03-02 | |
| | | |||
* | | Merge branch 'v8.5' | 2015-02-28 | |
|\| | |||
| * | Adding a test for bug #3612. | 2015-02-27 | |
| | | |||
| * | Test for bug #3249. | 2015-02-27 | |
| | | |||
| * | Fix test for #3467, I had moved it in a dumb way. | 2015-02-27 | |
| | | |||
| * | Add support so that the type of a match in an inductive type with let-in | 2015-02-27 | |
| | | | | | | | | | | | | | | | | | | 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. *) | ||
| * | Fixing first part of bug #3210 (inference of pattern-matching return | 2015-02-27 | |
| | | | | | | | | clause in the presence of let-ins in the arity of inductive type). | ||
| * | Fix test for #3848, still open. | 2015-02-27 | |
| | | |||
| * | Moving test for #3467 to closed after PMP's fix. | 2015-02-27 | |
| | | |||
| * | Fix test-suite files for bugs #2456 and #3593, still open. | 2015-02-27 | |
| | | |||
| * | Add test-suite file for #3649. | 2015-02-27 | |
| | | |||
| * | Moving tests for #2456 and #3593 to "opened" until they're fixed. | 2015-02-27 | |
| | | |||
| * | Made test for #3392 rely less on unification. | 2015-02-27 | |
| | | |||
| * | Moving test of #3848 to "opened". | 2015-02-27 | |
| | | |||
| * | Test for #2602, which seems now fixed. | 2015-02-26 | |
| | | |||
* | | Merge branch 'v8.5' | 2015-02-26 | |
|\| | |||
| * | Test for bug #3298. | 2015-02-26 | |
| | | |||
| * | Revert "Fixing bug #4035 (support for dependent destruction within ltac code)." | 2015-02-26 | |
| | | | | | | | | | | | | | | | | | | 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. | ||
| * | Moving test for bug #3681 as closed. | 2015-02-26 | |
| | | |||
| * | Univs: Fix Check calling the kernel to retype in the wrong environment. | 2015-02-24 | |
| | | | | | | | | Fixes bug #4089. | ||
* | | Merge branch 'v8.5' into trunk | 2015-02-23 | |
|\| | |||
| * | Fix some typos in comments. | 2015-02-23 | |
| | | |||
| * | Test for #3953 (subst in evar instances). | 2015-02-23 | |
| | | |||
| * | Fixing test #2830. | 2015-02-23 | |
| | | |||
| * | Fixing test for bug #3071. | 2015-02-23 | |
| | |