coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \|	Fixing Not_found on unknown bullet behavior.	Hugo Herbelin	2016-01-20
\| * \|	Fix bug #4420: check_types was losing universe constraints.	Matthieu Sozeau	2016-01-19
* \| \|	Universes algorithm : clarified comments	Jacques-Henri Jourdan	2016-01-17
* \| \|	Moving val_cast to Tacinterp.	Pierre-Marie Pédrot	2016-01-17
* \| \|	Getting rid of the awkward unpack mechanism from Genarg.	Pierre-Marie Pédrot	2016-01-17
* \| \|	Simplification and type-safety of Pcoq thanks to GADTs in Genarg.	Pierre-Marie Pédrot	2016-01-17
* \| \|	Exporting Genarg implementation in the API.	Pierre-Marie Pédrot	2016-01-17
* \| \|	Reimplementing Genarg safely.	Pierre-Marie Pédrot	2016-01-17
* \| \|	Adding a structure indexed by tags.	Pierre-Marie Pédrot	2016-01-17
* \| \|	Temporary commit getting rid of Obj.magic unsafety for Genarg.	Pierre-Marie Pédrot	2016-01-17
* \| \|	Removing dynamic entries from Pcoq.	Pierre-Marie Pédrot	2016-01-17
* \| \|	ML extensions use untyped representation of user entries.	Pierre-Marie Pédrot	2016-01-17
* \| \|	Separating the parsing of user-defined entries from their intepretation.	Pierre-Marie Pédrot	2016-01-16
* \| \|	Less type-unsafety in Pcoq.	Pierre-Marie Pédrot	2016-01-16
* \| \|	Tactic notation printing accesses all the token data.	Pierre-Marie Pédrot	2016-01-16
\| * \|	Thanks Hugo, but let's remain factual.	Maxime Dénès	2016-01-15
\| * \|	Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.	Maxime Dénès	2016-01-15
\| * \|	Minor edits in output of coqdep --help.	Maxime Dénès	2016-01-15
\| * \|	Fix #4408.	Pierre Courtieu	2016-01-15
\| * \|	Partially fixing #4408: coqdep --help is up to date.	Pierre Courtieu	2016-01-15
* \| \|	Removing constr generic argument.	Pierre-Marie Pédrot	2016-01-14
* \| \|	Removing ident and var generic arguments.	Pierre-Marie Pédrot	2016-01-14
* \| \|	Moving is_quantified_hypothesis to new proof engine.	Hugo Herbelin	2016-01-14
* \| \|	Updating and improving the documentation of intros patterns.	Hugo Herbelin	2016-01-14
* \| \|	Continuing 003fe3d5e on parsing positions.	Hugo Herbelin	2016-01-14
* \| \|	Changing "P is assumed" to "P is declared".	Hugo Herbelin	2016-01-14
* \| \|	Update in the documentation of parts of the code of destruct/induction.	Hugo Herbelin	2016-01-14
\| * \|	MMaps: remove it from final 8.5 release, since this new library isn't mature ...	Pierre Letouzey	2016-01-13
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\| \|
\| * \|	Fixing success of test for #3848 after move to directory "closed".	Hugo Herbelin	2016-01-13
\| * \|	Fixing #4467 (continued).	Hugo Herbelin	2016-01-13
\| * \|	Fixing #4467 (missing shadowing of variables in cases pattern).	Hugo Herbelin	2016-01-12
\| * \|	Fixing #4256 and #4484 (changes in evar-evar resolution made that new	Hugo Herbelin	2016-01-12
\| * \|	Reporting about the new tactical unshelve.	Hugo Herbelin	2016-01-12
\| * \|	Extend last commit: keyed unification uses full conversions on the applied co...	Matthieu Sozeau	2016-01-12
\| * \|	Extend Keyed Unification tests with the one from R. Krebbers.	Matthieu Sozeau	2016-01-12
\| * \|	Fix essential bug in new Keyed Unification mode reported by R. Krebbers.	Matthieu Sozeau	2016-01-12
\| * \|	Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.	Hugo Herbelin	2016-01-12
\| * \|	Documenting dtauto and dintuition.	Hugo Herbelin	2016-01-12
\| * \|	Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".	Hugo Herbelin	2016-01-12
\| * \|	Documenting option 'Set Bracketing Last Introduction Pattern'.	Hugo Herbelin	2016-01-12
\| * \|	restore documentation of admit	Enrico Tassi	2016-01-12
* \| \|	CLEANUP: removing unnecessary wrapper	Matej Kosik	2016-01-11
* \| \|	COMMENTS: added to the "Constrexpr.CCases" variant.	Matej Kosik	2016-01-11
* \| \|	CLEANUP: removing unused field	Matej Kosik	2016-01-11
* \| \|	merge	Matej Kosik	2016-01-11
\|\ \ \
\| * \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\| \| * \|	Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.	Matthieu Sozeau	2016-01-11
* \| \| \|	COMMENTS: of "Constr.case_info" type were updated.	Matej Kosik	2016-01-11
* \| \| \|	COMMENTS: added to the "Names.inductive" and "Names.constructor" types.	Matej Kosik	2016-01-11