aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Adding a "get" primitive to map signature.Gravatar Pierre-Marie Pédrot2016-02-03
* 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
| * Fixing bde12b70 about reporting ill-formed constructor.Gravatar Hugo Herbelin2016-01-26
| * 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
| * 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
| * 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 Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
| * Fix bug #4506. Using betadeltaiota_nolet might produce terms of the formGravatar Matthieu Sozeau2016-01-23
* | Fixing a use of "clear" on an non-existing hypothesis in intro-patterns.Gravatar Hugo Herbelin2016-01-22
| * Restore warnings produced by the interpretation of the command lineGravatar Hugo Herbelin2016-01-22
* | New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).Gravatar Hugo Herbelin2016-01-21
| * 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
* | Fixing some problems with double induction.Gravatar Hugo Herbelin2016-01-21
* | 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
| * Clarifying the documentation of tactics "cbv" and "lazy".Gravatar Hugo Herbelin2016-01-20
| * 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
* | Reimplementing Genarg safely.Gravatar Pierre-Marie Pédrot2016-01-17
* | 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
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 03:52:04 +0000