| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-09-04 | Fix bug #3561, correct folding of env in context[] matching. | Matthieu Sozeau | |
| 2014-09-04 | Fix bug #3559, ensuring a canonical order of universe level quantifications when | Matthieu Sozeau | |
| introducing constants (e.g. Top.1 is always before Top.2), compatible with the one used before introduction of hMaps in LMap/LSet. | |||
| 2014-09-04 | Add test-suite file for Case derivation on primitive records. | Matthieu Sozeau | |
| 2014-09-04 | Add test suite files for closed bugs. | Matthieu Sozeau | |
| 2014-09-04 | Fix bug #3563, making syntactic matching of primitive projections | Matthieu Sozeau | |
| and their eta-expanded forms succeed, potentially filling parameter metavariables from the type information of the projected object. | |||
| 2014-09-03 | Yes another remaining clearing bug with 'apply in'. | Hugo Herbelin | |
| 2014-09-03 | Test-suite for bug #2818. | Pierre-Marie Pédrot | |
| 2014-09-02 | Adding a test-suite for second-order matching order and indexes. | Pierre-Marie Pédrot | |
| 2014-09-02 | Another fix than 19a7a5789c to avoid descend_in_conjunction to use | Hugo Herbelin | |
| fresh names interferring with names later generated in intropatterns (as introduced in 72498d6d68ac which passed "clenv_refine_in continued by pattern introduction" to descend_in_conjunction while only a pure clenv_refine was passed before). The 72498d6d68ac version was generating fresh names in the wrong order (morally-private names for descend_in_conjunction before user-level names in clenv_refine_in). The 19a7a5789c fix was introducing expressions not handled by the refine from logic.ml. In particular, this fixes RelationAlgebra. | |||
| 2014-09-02 | An apply test. | Hugo Herbelin | |
| 2014-08-30 | Simplify even further the declaration of primitive projections, | Matthieu Sozeau | |
| now done entirely using declare_mind, which declares the associated constants for primitive records. This avoids a hack related to elimination schemes and ensures that the forward references to constants in the mutual inductive entry are properly declared just after the inductive. This also clarifies (and simplifies) the code of term_typing for constants which does not have to deal with building or checking projections anymore. Also fix printing of universes showing the de Bruijn encoding in a few places. | |||
| 2014-08-29 | Not using a "cut" in descend_in_conjunctions induced more success. We | Hugo Herbelin | |
| at least remove the successes obtained by trivial unification of a meta with the goal, so as to avoid surprising results. We generalize this to variables which will only eventually be replaced by metas. | |||
| 2014-08-29 | Add test-suite file. Compute the name for the record binder in the | Matthieu Sozeau | |
| eta-expanded version of a projection as before. | |||
| 2014-08-28 | Fix bugs #3484 and #3546. | Matthieu Sozeau | |
| The unification oracle now prefers unfolding the eta-expanded form of a projection over the primitive projection, and allows first-order unification on applications of constructors of primitive records, in case eta-conversion fails (disabled by previous patch on eta). | |||
| 2014-08-28 | There are some occurs-check cases that can be handled by imitation (using ↵ | Matthieu Sozeau | |
| pruning), hence do not entirely prevent solve_simple_eqn in case of apparent occurs-check but backtrack to eqappr on OccurCheck failures (problem found in Ssreflect). | |||
| 2014-08-28 | Fixing an unnatural selection of subterms larger than expected in the | Hugo Herbelin | |
| presence of let-ins. | |||
| 2014-08-28 | Adding test-suite for bug #3212. | Pierre-Marie Pédrot | |
| 2014-08-26 | Add a regression test for 3427 | Jason Gross | |
| 2014-08-25 | Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible | Matthieu Sozeau | |
| to match on a primitive projection application c.(p) using "?f _", binding f to (fun x => x.(p)) with the correct typing. | |||
| 2014-08-25 | Fix computation of dangling constraints at the end of a proof (bug #3531). | Matthieu Sozeau | |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross | |
| It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar). | |||
| 2014-08-25 | instanciation is French, instantiation is English | Jason Gross | |
| 2014-08-25 | Grammar: "avoiding to" isn't proper, either | Jason Gross | |
| 2014-08-25 | Fixing a bug introduced in the extension of 'apply in' + simplifying code. | Hugo Herbelin | |
| 2014-08-23 | Fix test-suite file. | Matthieu Sozeau | |
| 2014-08-18 | Fixing unification of subterms identified by patterns. | Hugo Herbelin | |
| 2014-08-18 | A reorganization of the "assert" tactics (hopefully uniform naming | Hugo Herbelin | |
| scheme, redundancies, possibility of chaining a tactic knowing the name of introduced hypothesis, new proof engine). | |||
| 2014-08-18 | Fix test-suite file. | Matthieu Sozeau | |
| 2014-08-18 | Fix test-suite files. | Matthieu Sozeau | |
| 2014-08-18 | Fix test-suite file. | Matthieu Sozeau | |
| 2014-08-16 | Fixing too restrictive detection of resolution of evars in "apply in" | Hugo Herbelin | |
| (revealed by contribution PTSF). | |||
| 2014-08-14 | Restrict eta-conversion to inductive records, fixing bug #3310. | Matthieu Sozeau | |
| 2014-08-13 | Fix test-suite files according to new parsing rule for application of primitive | Matthieu Sozeau | |
| projections. | |||
| 2014-08-12 | Upgrading output tests. | Hugo Herbelin | |
| output/Arguments.v output/ArgumentsScope.v output/Arguments_renaming.v output/Cases.v output/Implicit.v output/PrintInfos.v output/TranspModType.v Main changes: monomorphic -> not universe polymorphic, Peano vs Nat | |||
| 2014-08-12 | Bug #3469: fixing unterminated comment. | Hugo Herbelin | |
| 2014-08-12 | In bug #2406, renouncing to test failure of parsing error. | Hugo Herbelin | |
| (AFAIU, it is the table of supported unicode characters which has to be upgraded anyway.) | |||
| 2014-08-09 | Fix unification which was failing when unifying a primitive projection against | Matthieu Sozeau | |
| its expansion if it could reduce (fixes bug #3480). | |||
| 2014-08-08 | Fix evarconv not applying eta when it used to. Fixes bug#3319. | Matthieu Sozeau | |
| 2014-08-05 | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi | |
| par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2). | |||
| 2014-08-03 | Fixing #3483 (graceful failing with notations to non-constructors in "match"). | Hugo Herbelin | |
| 2014-07-31 | Finish fixes on notations and primitive projections, add test-suite files ↵ | Matthieu Sozeau | |
| for closed bugs | |||
| 2014-07-30 | Add test-suite file for bug #3439. | Matthieu Sozeau | |
| 2014-07-29 | Add test-suite file for bug 3454. | Matthieu Sozeau | |
| 2014-07-29 | Add test-suite file for bug #3453 | Matthieu Sozeau | |
| 2014-07-24 | fixup fakeide test-suite | Pierre Boutillier | |
| 2014-07-22 | Add test-suite file for guard condition on cofixpoints. | Maxime Dénès | |
| 2014-07-21 | Fixing output test-suite. | Pierre-Marie Pédrot | |
| 2014-07-21 | Adding a test-suite for bug #3422. | Pierre-Marie Pédrot | |
| 2014-07-16 | Adding a test-suite for bug #3416. | Pierre-Marie Pédrot | |
| 2014-07-11 | Fix Funind test-suite file after patch by Pierre. | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite