| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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 | 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 | |
| 2016-01-14 | Removing constr generic argument. | Pierre-Marie Pédrot | |
| 2016-01-14 | Removing ident and var generic arguments. | Pierre-Marie Pédrot | |
| 2016-01-14 | Moving is_quantified_hypothesis to new proof engine. | Hugo Herbelin | |
| 2016-01-14 | Updating and improving the documentation of intros patterns. | Hugo Herbelin | |
| In particular, documenting bracketing of last pattern on by default. | |||
| 2016-01-14 | Continuing 003fe3d5e on parsing positions. | Hugo Herbelin | |
| - Being stricter on the ordinal suffix accepted (only st for 1, 21, etc, nd for 2, 22, etc., etc.) - Reporting when the suffix is not the expected one (rather than considering that, e.g. 2st, is two tokens, a number then an identifier). | |||
| 2016-01-14 | Changing "P is assumed" to "P is declared". | Hugo Herbelin | |
| The term "assumed" refers more to the type of the object than to the name of the object. It is particularly misguiding when P:Prop since P is assumed would suggest that a proof of P is assumed, and not that the variable P itself is declared (see discussion with P. Castéran on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015). | |||
| 2016-01-14 | Update in the documentation of parts of the code of destruct/induction. | Hugo Herbelin | |
| 2016-01-13 | MMaps: remove it from final 8.5 release, since this new library isn't mature ↵ | Pierre Letouzey | |
| enough In particular, its interface might still change (in interaction with interested colleagues). So let's not give it too much visibility yet. Instead, I'll turn it as an opam packages for now. | |||
| 2016-01-13 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-13 | Fixing success of test for #3848 after move to directory "closed". | Hugo Herbelin | |
| 2016-01-13 | Fixing #4467 (continued). | Hugo Herbelin | |
| Function is_constructor was not properly fixed. Additionally, this fixes a problem with the 8.5 interpretation of in-pattern (see Cases.v). | |||
| 2016-01-12 | Fixing #4467 (missing shadowing of variables in cases pattern). | Hugo Herbelin | |
| This fixes a TODO in map_constr_expr_with_binders, a bug in is_constructor, as well as a bug and TODOS in ids_of_cases_indtype. | |||
| 2016-01-12 | Fixing #4256 and #4484 (changes in evar-evar resolution made that new | Hugo Herbelin | |
| evars were created making in turn that evars formerly recognized as pending were not anymore in the list of pending evars). This also fixes the reopening of #3848. See comments on #4484 for details. | |||
| 2016-01-12 | Reporting about the new tactical unshelve. | Hugo Herbelin | |
| 2016-01-12 | Extend last commit: keyed unification uses full conversions on the applied ↵ | Matthieu Sozeau | |
| constant and arguments _separately_. | |||
| 2016-01-12 | Extend Keyed Unification tests with the one from R. Krebbers. | Matthieu Sozeau | |
| 2016-01-12 | Fix essential bug in new Keyed Unification mode reported by R. Krebbers. | Matthieu Sozeau | |
| [rewrite] was calling find_suterm using the wrong unification flags, not allowing full delta in unification of terms with the right keys as desired. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |