aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| * Adding a test for bug #4378.Gravatar Pierre-Marie Pédrot2016-01-24
| |
| * Fixing bug #4495: Failed assertion in metasyntax.ml.Gravatar Pierre-Marie Pédrot2016-01-24
| | | | | | | | | | | | 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.
| * Fixing bug #4511: evar tactic can create non-typed evars.Gravatar Pierre-Marie Pédrot2016-01-24
| |
| * Fix bug #4503: mixing universe polymorphic and monomorphicGravatar Matthieu Sozeau2016-01-23
| | | | | | | | variables and definitions in sections is unsupported.
| * Fix bug #4519: oops, global shadowed local universe level bindings.Gravatar Matthieu Sozeau2016-01-23
| |
| * Implement support for universe binder lists in Instance and Program ↵Gravatar Matthieu Sozeau2016-01-23
| | | | | | | | Fixpoint/Definition.
| * Fix bug #4506. Using betadeltaiota_nolet might produce terms of the formGravatar Matthieu Sozeau2016-01-23
| | | | | | | | | | (let x := t in u) a that should be reduced. Maybe a different decomposition/reduction primitive should be used instead.
* | Fixing a use of "clear" on an non-existing hypothesis in intro-patterns.Gravatar Hugo Herbelin2016-01-22
| | | | | | | | | | It was not detected because of a "bug" in clear checking the existence of the hypothesis only at interpretation time (not at execution time).
| * Restore warnings produced by the interpretation of the command lineGravatar Hugo Herbelin2016-01-22
| | | | | | | | | | | | | | (e.g. with deprecated options such as -byte, etc.) since I guess this is what we expect. Was probably lost in 81eb133d64ac81cb.
* | New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).Gravatar Hugo Herbelin2016-01-21
| | | | | | | | | | - Fixing dead code, doc. - Relaxing constraints on using an as-tuple in inversion.
| * Compile OS X binaries without native_compute support.Gravatar Maxime Dénès2016-01-21
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| | | | | | | | | | | | | | | | | | | | 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.
* | Fixing some problems with double induction.Gravatar Hugo Herbelin2016-01-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Code simplification in elim.ml.Gravatar Hugo Herbelin2016-01-20
| |
* | Fixing a bug with introduction patterns over inductive types containing let-ins.Gravatar Hugo Herbelin2016-02-18
| |
| * Update cic.mli MD5 after header update.Gravatar Maxime Dénès2016-01-20
| |
| * Update version number in configure.Gravatar Maxime Dénès2016-01-20
| |
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
| * Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.Gravatar Maxime Dénès2016-01-20
| |
| * Documenting Set Bullet Behavior.Gravatar Hugo Herbelin2016-01-20
| | | | | | | | | | | | This is useful for restoring bullets after e.g. loading ssreflect. Hoping Arnaud is ok in documenting it.
| * Clarifying the documentation of tactics "cbv" and "lazy".Gravatar Hugo Herbelin2016-01-20
| | | | | | | | Following a discussion on coq-club on Jan 13, 2016.
| * Fixing Not_found on unknown bullet behavior.Gravatar Hugo Herbelin2016-01-20
| |
| * Fix bug #4420: check_types was losing universe constraints.Gravatar Matthieu Sozeau2016-01-19
| |
* | Universes algorithm : clarified commentsGravatar Jacques-Henri Jourdan2016-01-17
| |
* | Moving val_cast to Tacinterp.Gravatar Pierre-Marie Pédrot2016-01-17
| |
* | Getting rid of the awkward unpack mechanism from Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
| |
* | Simplification and type-safety of Pcoq thanks to GADTs in Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
| |
* | Exporting Genarg implementation in the API.Gravatar Pierre-Marie Pédrot2016-01-17
| | | | | | | | | | We can now use the expressivity of GADT to work around historical kludges of generic arguments.
* | Reimplementing Genarg safely.Gravatar Pierre-Marie Pédrot2016-01-17
| | | | | | | | | | | | 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.
* | Adding a structure indexed by tags.Gravatar Pierre-Marie Pédrot2016-01-17
| |
* | Temporary commit getting rid of Obj.magic unsafety for Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
| | | | | | | | This will allow an easier landing of the rewriting of Genarg.
* | Removing dynamic entries from Pcoq.Gravatar Pierre-Marie Pédrot2016-01-17
| |
* | ML extensions use untyped representation of user entries.Gravatar Pierre-Marie Pédrot2016-01-17
| |
* | Separating the parsing of user-defined entries from their intepretation.Gravatar Pierre-Marie Pédrot2016-01-16
| |
* | Less type-unsafety in Pcoq.Gravatar Pierre-Marie Pédrot2016-01-16
| |
* | Tactic notation printing accesses all the token data.Gravatar Pierre-Marie Pédrot2016-01-16
| |
| * Thanks Hugo, but let's remain factual.Gravatar Maxime Dénès2016-01-15
| |
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
| |
| * Minor edits in output of coqdep --help.Gravatar Maxime Dénès2016-01-15
| |
| * Fix #4408.Gravatar Pierre Courtieu2016-01-15
| | | | | | | | | | Removed documentation for broken -D -w (but the option are still there). Fixed documentation of others.
| * Partially fixing #4408: coqdep --help is up to date.Gravatar Pierre Courtieu2016-01-15
| |
* | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
| |
* | Removing ident and var generic arguments.Gravatar Pierre-Marie Pédrot2016-01-14
| |
* | Moving is_quantified_hypothesis to new proof engine.Gravatar Hugo Herbelin2016-01-14
| |
* | Updating and improving the documentation of intros patterns.Gravatar Hugo Herbelin2016-01-14
| | | | | | | | In particular, documenting bracketing of last pattern on by default.
* | Continuing 003fe3d5e on parsing positions.Gravatar Hugo Herbelin2016-01-14
| | | | | | | | | | | | | | - 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).
* | Changing "P is assumed" to "P is declared".Gravatar Hugo Herbelin2016-01-14
| | | | | | | | | | | | | | | | 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).
* | Update in the documentation of parts of the code of destruct/induction.Gravatar Hugo Herbelin2016-01-14
| |
| * MMaps: remove it from final 8.5 release, since this new library isn't mature ↵Gravatar Pierre Letouzey2016-01-13
| | | | | | | | | | | | | | | | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-23 00:53:21 +0000