| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-02-02 | Removing a source of type-unsafeness in Pcoq. | Pierre-Marie Pédrot | |
| 2016-02-01 | Infering atomic ML entries from their grammar. | Pierre-Marie Pédrot | |
| 2016-01-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-27 | Fix bug #4537: Coq 8.5 is slower in typeclass resolution. | Pierre-Marie Pédrot | |
| The performance enhancement introduced by a895b2c0 for non-polymorphic hints was actually causing a huge regression in the polymorphic case (and was marked as such). We fix this by only substituting the metas from the evarmap instead of the whole evarmap. | |||
| 2016-01-26 | Fixing bde12b70 about reporting ill-formed constructor. | Hugo Herbelin | |
| For instance, in Inductive I : nat -> nat -> Prop := C : forall z, let '(x,y) := z in x + y = 0. the computation of the number of arguments to I was made wrong in bde12b70. | |||
| 2016-01-24 | Tentative fix for bug #4522: Incorrect "Warning..." on windows. | Pierre-Marie Pédrot | |
| 2016-01-24 | Fixing bug #4373: coqdep does not know about .vio files. | Pierre-Marie Pédrot | |
| 2016-01-24 | Fixing bug #3826: "Incompatible module types" is uninformative. | Pierre-Marie Pédrot | |
| 2016-01-24 | Adding a test for bug #4378. | Pierre-Marie Pédrot | |
| 2016-01-24 | Fixing bug #4495: Failed assertion in metasyntax.ml. | Pierre-Marie Pédrot | |
| We simply handle the "break" in error messages. Not sure it is the proper bugfix though, we may want to be able to add breaks in such recursive notations. | |||
| 2016-01-24 | Fixing bug #4511: evar tactic can create non-typed evars. | Pierre-Marie Pédrot | |
| 2016-01-23 | Fix bug #4503: mixing universe polymorphic and monomorphic | Matthieu Sozeau | |
| variables and definitions in sections is unsupported. | |||
| 2016-01-23 | Fix bug #4519: oops, global shadowed local universe level bindings. | Matthieu Sozeau | |
| 2016-01-23 | Implement support for universe binder lists in Instance and Program ↵ | Matthieu Sozeau | |
| Fixpoint/Definition. | |||
| 2016-01-23 | Fix bug #4506. Using betadeltaiota_nolet might produce terms of the form | Matthieu Sozeau | |
| (let x := t in u) a that should be reduced. Maybe a different decomposition/reduction primitive should be used instead. | |||
| 2016-01-22 | Fixing a use of "clear" on an non-existing hypothesis in intro-patterns. | Hugo Herbelin | |
| It was not detected because of a "bug" in clear checking the existence of the hypothesis only at interpretation time (not at execution time). | |||
| 2016-01-22 | Restore warnings produced by the interpretation of the command line | Hugo Herbelin | |
| (e.g. with deprecated options such as -byte, etc.) since I guess this is what we expect. Was probably lost in 81eb133d64ac81cb. | |||
| 2016-01-21 | New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern). | Hugo Herbelin | |
| - Fixing dead code, doc. - Relaxing constraints on using an as-tuple in inversion. | |||
| 2016-01-21 | Compile OS X binaries without native_compute support. | Maxime Dénès | |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-21 | Stronger invariants on the use of the introduction pattern (pat1,...,patn). | Hugo Herbelin | |
| The length of the pattern should now be exactly the number of assumptions and definitions introduced by the destruction or induction, including the induction hypotheses in case of an induction. Like for pattern-matching, the local definitions in the argument of the constructor can be skipped in which case a name is automatically created for these. | |||
| 2016-01-21 | Fixing some problems with double induction. | Hugo Herbelin | |
| Basically, the hypotheses were treated in an incorrect order, with a hack for sometimes put them again in the right order, resulting in failures and redundant hypotheses. Status unclear, because this new version is incompatible except in simple cases like a double induction on two "nat". Fixing the bug incidentally simplify the code, relying on the deprecation since 8.4 to allow not to ensure a compatibility (beyond the simple situation of a double induction on simple datatypes). See file induct.v for effect of changes. | |||
| 2016-01-20 | Code simplification in elim.ml. | Hugo Herbelin | |
| 2016-02-18 | Fixing a bug with introduction patterns over inductive types containing let-ins. | Hugo Herbelin | |
| 2016-01-20 | Update cic.mli MD5 after header update. | Maxime Dénès | |
| 2016-01-20 | Update version number in configure. | Maxime Dénès | |
| 2016-01-20 | Update copyright headers. | Maxime Dénès | |
| 2016-01-20 | Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500. | Maxime Dénès | |
| 2016-01-20 | Documenting Set Bullet Behavior. | Hugo Herbelin | |
| This is useful for restoring bullets after e.g. loading ssreflect. Hoping Arnaud is ok in documenting it. | |||
| 2016-01-20 | Clarifying the documentation of tactics "cbv" and "lazy". | Hugo Herbelin | |
| Following a discussion on coq-club on Jan 13, 2016. | |||
| 2016-01-20 | Fixing Not_found on unknown bullet behavior. | Hugo Herbelin | |
| 2016-01-19 | Fix bug #4420: check_types was losing universe constraints. | Matthieu Sozeau | |
| 2016-01-17 | Universes algorithm : clarified comments | Jacques-Henri Jourdan | |
| 2016-01-17 | Moving val_cast to Tacinterp. | Pierre-Marie Pédrot | |
| 2016-01-17 | Getting rid of the awkward unpack mechanism from Genarg. | Pierre-Marie Pédrot | |
| 2016-01-17 | Simplification and type-safety of Pcoq thanks to GADTs in Genarg. | Pierre-Marie Pédrot | |
| 2016-01-17 | Exporting Genarg implementation in the API. | Pierre-Marie Pédrot | |
| We can now use the expressivity of GADT to work around historical kludges of generic arguments. | |||
| 2016-01-17 | Reimplementing Genarg safely. | Pierre-Marie Pédrot | |
| No more Obj.magic in Genarg. We leverage the expressivity of GADT coupled with dynamic tags to get rid of unsafety. For now the API did not change in order to port the legacy code more easily. | |||
| 2016-01-17 | Adding a structure indexed by tags. | Pierre-Marie Pédrot | |
| 2016-01-17 | Temporary commit getting rid of Obj.magic unsafety for Genarg. | Pierre-Marie Pédrot | |
| This will allow an easier landing of the rewriting of Genarg. | |||
| 2016-01-17 | Removing dynamic entries from Pcoq. | Pierre-Marie Pédrot | |
| 2016-01-17 | ML extensions use untyped representation of user entries. | Pierre-Marie Pédrot | |
| 2016-01-16 | Separating the parsing of user-defined entries from their intepretation. | Pierre-Marie Pédrot | |
| 2016-01-16 | Less type-unsafety in Pcoq. | Pierre-Marie Pédrot | |
| 2016-01-16 | Tactic notation printing accesses all the token data. | Pierre-Marie Pédrot | |
| 2016-01-15 | Thanks Hugo, but let's remain factual. | Maxime Dénès | |
| 2016-01-15 | Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. | Maxime Dénès | |
| 2016-01-15 | Minor edits in output of coqdep --help. | Maxime Dénès | |
| 2016-01-15 | Fix #4408. | Pierre Courtieu | |
| Removed documentation for broken -D -w (but the option are still there). Fixed documentation of others. | |||
| 2016-01-15 | Partially fixing #4408: coqdep --help is up to date. | Pierre Courtieu | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |