aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2016-01-13MMaps: remove it from final 8.5 release, since this new library isn't mature ...Pierre Letouzey
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-13Fixing success of test for #3848 after move to directory "closed".Hugo Herbelin
2016-01-13Fixing #4467 (continued).Hugo Herbelin
2016-01-12Fixing #4467 (missing shadowing of variables in cases pattern).Hugo Herbelin
2016-01-12Fixing #4256 and #4484 (changes in evar-evar resolution made that newHugo Herbelin
2016-01-12Reporting about the new tactical unshelve.Hugo Herbelin
2016-01-12Extend last commit: keyed unification uses full conversions on the applied co...Matthieu Sozeau
2016-01-12Extend Keyed Unification tests with the one from R. Krebbers.Matthieu Sozeau
2016-01-12Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Matthieu Sozeau
2016-01-12Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.Hugo Herbelin
2016-01-12Documenting dtauto and dintuition.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 03:21:41 +0000