aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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).
* 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.
* 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.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\|
| * Fixing success of test for #3848 after move to directory "closed".Gravatar Hugo Herbelin2016-01-13
| |
| * Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
| | | | | | | | | | Function is_constructor was not properly fixed. Additionally, this fixes a problem with the 8.5 interpretation of in-pattern (see Cases.v).
| * Fixing #4467 (missing shadowing of variables in cases pattern).Gravatar Hugo Herbelin2016-01-12
| | | | | | | | | | 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.
| * Fixing #4256 and #4484 (changes in evar-evar resolution made that newGravatar Hugo Herbelin2016-01-12
| | | | | | | | | | | | | | | | 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.
| * Reporting about the new tactical unshelve.Gravatar Hugo Herbelin2016-01-12
| |
| * Extend last commit: keyed unification uses full conversions on the applied ↵Gravatar Matthieu Sozeau2016-01-12
| | | | | | | | constant and arguments _separately_.
| * Extend Keyed Unification tests with the one from R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
| |
| * Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
| | | | | | | | | | [rewrite] was calling find_suterm using the wrong unification flags, not allowing full delta in unification of terms with the right keys as desired.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 11:27:04 +0000