aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Adding a "get" primitive to map signature.Gravatar Pierre-Marie Pédrot2016-02-03
| | | | | It is similar to find but raises an assertion failure instead of a Not_found when the element is not encountered. Using it will give stronger invariants.
* Removing a source of type-unsafeness in Pcoq.Gravatar Pierre-Marie Pédrot2016-02-02
|
* Infering atomic ML entries from their grammar.Gravatar Pierre-Marie Pédrot2016-02-01
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\
| * Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Gravatar Pierre-Marie Pédrot2016-01-27
| | | | | | | | | | | | | | 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.
| * Fixing bde12b70 about reporting ill-formed constructor.Gravatar Hugo Herbelin2016-01-26
| | | | | | | | | | | | | | | | 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.
| * Tentative fix for bug #4522: Incorrect "Warning..." on windows.Gravatar Pierre-Marie Pédrot2016-01-24
| |
| * Fixing bug #4373: coqdep does not know about .vio files.Gravatar Pierre-Marie Pédrot2016-01-24
| |
| * Fixing bug #3826: "Incompatible module types" is uninformative.Gravatar Pierre-Marie Pédrot2016-01-24
| |
| * 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 13:02:28 +0000