| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | 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 | |
| 2015-05-09 | Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default). | Hugo Herbelin | |
| 2015-05-09 | Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for | Hugo Herbelin | |
| preserving compatibility of subst after #4214 being solved. | |||
| 2015-05-06 | Fixing treatment of recursive equations damaged by 857e82b2ca0d1. | Hugo Herbelin | |
| Improving treatment of recursive equations compared to 8.4 (see test-suite). Experimenting not to unfold local defs ever in subst. (+ Slight simplification in checking reflexive equalities only once). | |||
| 2015-05-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-05-01 | Fixing computation of implicit arguments by position in fixpoints (#4217). | Hugo Herbelin | |
| 2015-05-01 | Giving to "subst" a more natural semantic (fixing #4214) by using all | Hugo Herbelin | |
| equalities in configurations like x=y x=z === P(x,y,z) where it now produces === P(z,z,z) In particular (equations are processed from most ancient to most recent). Thanks to this, a "repeat subst" can just be a "subst" in List.v. Incidentally: moved a nf_enter to enter in subst_one, since the latter is normally called from other tactics having normalized evars. | |||
| 2015-04-22 | Tactical `progress` compares term up to potentially equalisable universes. | Arnaud Spiwack | |
| Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593. As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation. | |||
| 2015-04-22 | Test for #4198 (appcontext in return clause of match). | Hugo Herbelin | |
| 2015-04-21 | Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argument | Hugo Herbelin | |
| in the presence of let-ins). | |||
| 2015-04-17 | Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of several | Hugo Herbelin | |
| libraries at once (see #4193). | |||
| 2015-04-16 | Test for bug #4190. | Pierre-Marie Pédrot | |
| 2015-04-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-04-10 | Test for bug #3199. | Pierre-Marie Pédrot | |
| 2015-04-09 | Better test-suite files, removing reliance on admit. | Matthieu Sozeau | |
| 2015-04-09 | Fix declarations of instances to perform restriction of universe | Matthieu Sozeau | |
| instances as definitions and lemmas do (fixes bug# 4121). | |||
| 2015-04-09 | Add test-suite file for bug #4120. | Matthieu Sozeau | |
| 2015-04-09 | Merge branch 'v8.5' into trunk | Pierre Letouzey | |
| 2015-04-06 | Test for bug #3815. | Pierre-Marie Pédrot | |
| 2015-04-01 | Fixing test-suite. | Pierre-Marie Pédrot | |
| 2015-03-31 | Fixing test-suite. | Pierre-Marie Pédrot | |
| 2015-03-30 | Merge branch 'v8.5' into trunk | Enrico Tassi | |
| 2015-03-30 | camlp4: grep away warnings in output/* tests | Enrico Tassi | |
| 2015-03-29 | Adding test for bug #4165. | Pierre-Marie Pédrot | |
| 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). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite