aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-01-24Fixing bug #3826: "Incompatible module types" is uninformative.Pierre-Marie Pédrot
2016-01-24Adding a test for bug #4378.Pierre-Marie Pédrot
2016-01-24Fixing bug #4495: Failed assertion in metasyntax.ml.Pierre-Marie Pédrot
2016-01-24Fixing bug #4511: evar tactic can create non-typed evars.Pierre-Marie Pédrot
2016-01-23Fix bug #4503: mixing universe polymorphic and monomorphicMatthieu Sozeau
2016-01-23Fix bug #4519: oops, global shadowed local universe level bindings.Matthieu Sozeau
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-23Fix bug #4506. Using betadeltaiota_nolet might produce terms of the formMatthieu Sozeau
2016-01-22Fixing a use of "clear" on an non-existing hypothesis in intro-patterns.Hugo Herbelin
2016-01-22Restore warnings produced by the interpretation of the command lineHugo Herbelin
2016-01-21New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).Hugo Herbelin
2016-01-21Compile OS X binaries without native_compute support.Maxime Dénès
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-21Stronger invariants on the use of the introduction pattern (pat1,...,patn).Hugo Herbelin
2016-01-21Fixing some problems with double induction.Hugo Herbelin
2016-01-20Code simplification in elim.ml.Hugo Herbelin
2016-02-18Fixing a bug with introduction patterns over inductive types containing let-ins.Hugo Herbelin
2016-01-20Update cic.mli MD5 after header update.Maxime Dénès
2016-01-20Update version number in configure.Maxime Dénès
2016-01-20Update copyright headers.Maxime Dénès
2016-01-20Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.Maxime Dénès
2016-01-20Documenting Set Bullet Behavior.Hugo Herbelin
2016-01-20Clarifying the documentation of tactics "cbv" and "lazy".Hugo Herbelin
2016-01-20Fixing Not_found on unknown bullet behavior.Hugo Herbelin
2016-01-19Fix bug #4420: check_types was losing universe constraints.Matthieu Sozeau
2016-01-17Universes algorithm : clarified commentsJacques-Henri Jourdan
2016-01-17Moving val_cast to Tacinterp.Pierre-Marie Pédrot
2016-01-17Getting rid of the awkward unpack mechanism from Genarg.Pierre-Marie Pédrot
2016-01-17Simplification and type-safety of Pcoq thanks to GADTs in Genarg.Pierre-Marie Pédrot
2016-01-17Exporting Genarg implementation in the API.Pierre-Marie Pédrot
2016-01-17Reimplementing Genarg safely.Pierre-Marie Pédrot
2016-01-17Adding a structure indexed by tags.Pierre-Marie Pédrot
2016-01-17Temporary commit getting rid of Obj.magic unsafety for Genarg.Pierre-Marie Pédrot
2016-01-17Removing dynamic entries from Pcoq.Pierre-Marie Pédrot
2016-01-17ML extensions use untyped representation of user entries.Pierre-Marie Pédrot
2016-01-16Separating the parsing of user-defined entries from their intepretation.Pierre-Marie Pédrot
2016-01-16Less type-unsafety in Pcoq.Pierre-Marie Pédrot
2016-01-16Tactic notation printing accesses all the token data.Pierre-Marie Pédrot
2016-01-15Thanks Hugo, but let's remain factual.Maxime Dénès
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2016-01-15Minor edits in output of coqdep --help.Maxime Dénès
2016-01-15Fix #4408.Pierre Courtieu
2016-01-15Partially fixing #4408: coqdep --help is up to date.Pierre Courtieu
2016-01-14Removing constr generic argument.Pierre-Marie Pédrot
2016-01-14Removing ident and var generic arguments.Pierre-Marie Pédrot
2016-01-14Moving is_quantified_hypothesis to new proof engine.Hugo Herbelin
2016-01-14Updating and improving the documentation of intros patterns.Hugo Herbelin
2016-01-14Continuing 003fe3d5e on parsing positions.Hugo Herbelin
2016-01-14Changing "P is assumed" to "P is declared".Hugo Herbelin
2016-01-14Update in the documentation of parts of the code of destruct/induction.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 22:45:58 +0000