| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-07-22 | Extraction: fix primitive projection extraction. | Matthieu Sozeau | |
| Use expand projection to come back to the projection-as-constant encoding, dealing with parameters correctly. | |||
| 2015-07-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-07-16 | Refining 71def2f8 on too strong occur-check limiting evar-evar | Hugo Herbelin | |
| unification in tactics. The relaxing of occur-check was ok but was leading trivial problems of the form ?X[?Meta] = ?X[?Meta] to enter a complex Evar-ization into ?X[?Meta] = ?X[?Y], ?Meta:=?Y which consider_remaining_unif_problems was not any more able to deal with. Doing quick: treat the trivial cases ?X[args] = ?X[args] in an ad hoc way, so that it behaves as if the occur-check had not been restricted. | |||
| 2015-07-16 | Remove old test file for #3819 (now fixed). | Maxime Dénès | |
| 2015-07-16 | Fixing bug #4240 (closure_of_filter was not ensuring refinement of | Hugo Herbelin | |
| former filter after 48509b61 and 3cd718c, because filtered let-ins were not any longer preserved). | |||
| 2015-07-16 | Test file for #3819. | Maxime Dénès | |
| 2015-07-09 | Kernel/Checker: Cleanup fixes of substitutions due to let-ins. | Matthieu Sozeau | |
| Avoid undeeded large substitutions, and add test-suite file for fixed bug 4283 in closed/ | |||
| 2015-07-09 | Kernel: primitive projections handling of let-ins | Matthieu Sozeau | |
| Fixes bug #4176 (actually two bugs in one) Correct computation of the type of primitive projections in presence of let-ins. | |||
| 2015-07-07 | Checker: Fix bug #4282 | Matthieu Sozeau | |
| Adapt to new [projection] abstract type comprising a constant and a boolean. | |||
| 2015-07-07 | Univs: bug fix. | Matthieu Sozeau | |
| Missing universe substitutions of mind_params_ctxt when typechecking cases, which appeared only when let-ins were used. | |||
| 2015-07-07 | test-suite: Fix test-suite Makefile | Matthieu Sozeau | |
| Using relative path for coqlib, for some reason this fails on Mac OS X. Took the easiest way to fix it. | |||
| 2015-07-06 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-07-06 | Temporarily disable test file for #3922. | Maxime Dénès | |
| 2015-07-06 | Test case for #4203, fixed by commit a51cce36. | Maxime Dénès | |
| 2015-07-02 | Remove a line from test-suite. | Maxime Dénès | |
| Triggers a bug in declarative mode. Waiting for someone to volunteer and fix the bug, but meanwhile I'm trying to fix the test-suite. | |||
| 2015-07-02 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-07-01 | Notation: use same level for "@" in constr: and pattern: (Close: #4272) | Enrico Tassi | |
| A possible script breakage can occur if one has a notation at level 11 that is also right associative (now 11 is left associative). Thanks Georges for debugging that. | |||
| 2015-06-30 | Another missing Fail and comment in test-suite. | Maxime Dénès | |
| 2015-06-30 | Missing "Fail" in test-suite. | Maxime Dénès | |
| 2015-06-29 | Fix test file for #4214 which was fixed by Hugo. | Maxime Dénès | |
| 2015-06-29 | Better test case by PMP for #3948. | Maxime Dénès | |
| 2015-06-28 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-06-28 | Fix incompleteness of conversion used by evarconv | Matthieu Sozeau | |
| In case we need to backtrack on universe inconsistencies when converting two (incompatible) instances of the same constant and unfold them. Bug reported by Amin Timany. | |||
| 2015-06-26 | Fix bug #4254 with the help of J.H. Jourdan | Matthieu Sozeau | |
| 1) We now _assign_ the smallest possible arities to mutual inductive types and eventually add leq constraints on the user given arities. Remove useless limitation on instantiating algebraic universe variables with their least upper bound if they have upper constraints as well. 2) Do not remove non-recursive variables when computing minimal levels of inductives. 3) Avoid modifying user-given arities if not necessary to compute the minimal level of an inductive. 4) We correctly solve the recursive equations taking into account the user-declared level. | |||
| 2015-06-24 | Extend 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-06-24 | Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8. | Maxime Dénès | |
| 2015-06-24 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-06-23 | Fixing incompatibility introduced with simpl in commit 364decf59c1 (or | Hugo Herbelin | |
| maybe ca71714). Goal 2=2+2. match goal with |- (_ = ?c) => simpl c end. was working in 8.4 but was failing in 8.5beta2. Note: Changes in tacintern.ml are otherwise purely cosmetic. | |||
| 2015-06-22 | Merge remote-tracking branch 'forge/v8.5' | Pierre Boutillier | |
| 2015-06-11 | Add test-suite file for bug #3446. | Matthieu Sozeau | |
| 2015-06-09 | STM: states coming from workers have no proof terminators (Close #4246) | Enrico Tassi | |
| Hence we reuse the ones in master. | |||
| 2015-06-09 | STM: silly mistake in jumping back to an old state (Close #4249) | Enrico Tassi | |
| 2015-06-02 | Adding a test for bug #4057. | Pierre-Marie Pédrot | |
| 2015-06-01 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-05-29 | Flag -test-mode intended to be used for ad-hoc prints in test-suite | Enrico Tassi | |
| Of course there is an exception to the previous commit. Fail used to print even if silenced but loading a vernac file. This behavior is useful only in tests, hence this flag. | |||
| 2015-05-28 | STM: preserve branch name on edit (Close: #4245, #4246) | Enrico Tassi | |
| 2015-05-28 | Test for 4159 | Enrico Tassi | |
| 2015-05-19 | Test for bug #4116. | Pierre-Marie Pédrot | |
| 2015-05-18 | Removing test for opened bugs that were already present in the closed ↵ | Pierre-Marie Pédrot | |
| test-suite. | |||
| 2015-05-18 | Tentative fix for #3461: Anomaly: Uncaught exception ↵ | Pierre-Marie Pédrot | |
| Pretype_errors.PretypeError. Instad of trying to print the exception, we raise it in the tactic monad. | |||
| 2015-05-18 | Removing option -no-native-compiler from test #3539 since this option is now | Hugo Herbelin | |
| negated into -native-compiler. | |||
| 2015-05-15 | Removing option -no-native-compiler from test #3539 since this option is now | Hugo Herbelin | |
| negated into -native-compiler. | |||
| 2015-05-15 | Turning "Set Regular Subst Tactic" on by default (for 8.6). | Hugo Herbelin | |
| 2015-05-15 | Merge v8.5 into trunk | Hugo Herbelin | |
| Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API) | |||
| 2015-05-14 | #3953 now closed. | Hugo Herbelin | |
| 2015-05-13 | Fixing bug #4216: | Pierre-Marie Pédrot | |
| Internal error: Anomaly: Uncaught exception Not_found. Please report. An evarmap was lost because of an unsound typing primitive. | |||
| 2015-05-13 | Better fixing #4198 such that the term to match is looked for before | Hugo Herbelin | |
| the predicate, thus respecting the visual left-to-right top-down order (see a45bd5981092). This fixes CFGV. | |||
| 2015-05-12 | Extraction: fix the detection of the "polyprop" situation | Pierre Letouzey | |
| The ~polyprop argument wasn't propagated properly anymore, leading the extraction to try to operate on situations it cannot handle (yet). Cf Table.error_singleton_become_prop for more details. Regression test added. | |||
| 2015-05-12 | Test for bug #4234. | Pierre-Marie Pédrot | |
| 2015-05-11 | Test for bug #4232. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite