coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Checker: no more -I kernel via a few symlinks (for Names and Esubst)	Pierre Letouzey	2016-05-31
*	Extraction : add a location in the error message about polyprop	Pierre Letouzey	2016-05-30
*	Update required OCaml version in configure.	Maxime Dénès	2016-05-26
*	typos	Enrico Tassi	2016-05-23
*	Extraction: code cleanup in Common	Pierre Letouzey	2016-05-20
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-20
\|\
\| *	native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
\| *	Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
* \|	native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
* \|	Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
\| *	adding "user-contrib" directory to ".gitignore"	Matej Kosik	2016-05-19
\| *	Unicode.ascii_of_ident is now truly injective	Pierre Letouzey	2016-05-19
* \|	Unicode.ascii_of_ident is now truly injective	Pierre Letouzey	2016-05-19
* \|	Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/...	Pierre Letouzey	2016-05-19
* \|	Putting all the tactics exported by the Tactics module in the new monad API.	Pierre-Marie Pédrot	2016-05-17
\|\ \
\| * \|	Removing some compatibility layers in Tactics.	Pierre-Marie Pédrot	2016-05-17
\| * \|	Removing the old refine tactic from the Tactics module.	Pierre-Marie Pédrot	2016-05-17
\| * \|	Put the "move" tactic in the monad.	Pierre-Marie Pédrot	2016-05-17
\| * \|	Put the "change" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \|	Put the "specialize_eq" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \|	Put the "generalize dependent" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \|	Put the "generalize" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \|	Put the "cofix" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \|	Put the "*_cast_no_check" tactics in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \|	Put the "exact" family of tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \|	Put the "fix" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \|	Put the "exact_constr" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \|	Put the "clear" tactic into the monad.	Pierre-Marie Pédrot	2016-05-16
\|/ /
\| *	Fix bug #4737: cycle tactic doesn't like zero goals.	Pierre-Marie Pédrot	2016-05-16
* \|	Generate more user-readable tactic notation kernel names.	Pierre-Marie Pédrot	2016-05-16
* \|	Merge pull request #170 from relrod/patch-1	Pierre-Marie Pédrot	2016-05-16
\|\ \
\| * \|	Fix a really small doc typo	Ricky Elrod	2016-05-15
\|/ /
\| *	Removing unexcepted activation of option "Regular Subst Tactic", since	Hugo Herbelin	2016-05-14
\| *	More hints on how to fix compatibility issues.	Hugo Herbelin	2016-05-14
* \|	Hack in TACTIC EXTEND to maintain the 8.5 behaviour on badly designed arguments.	Pierre-Marie Pédrot	2016-05-14
* \|	Dyn: simplify API introducing an Easy submodule	Enrico Tassi	2016-05-13
* \|	More informative error message when interpreting ltac variables in terms.	Pierre-Marie Pédrot	2016-05-13
\| *	Small optimization in evar resolution.	Pierre-Marie Pédrot	2016-05-12
\| *	Fix bug #4722: Coq dies when encountering broken symbolic links.	Pierre-Marie Pédrot	2016-05-12
* \|	Thorough rewriting of the Pcoq API towards safety and static invariants.	Pierre-Marie Pédrot	2016-05-11
\|\ \
\| * \|	The grammar_extend function now registers unsynchronized extensions.	Pierre-Marie Pédrot	2016-05-11
\| * \|	Making the grammar command extend API purely functional.	Pierre-Marie Pédrot	2016-05-11
\| * \|	Moving the constr empty entry registering to the state-based API.	Pierre-Marie Pédrot	2016-05-11
\| * \|	Turning the grammar extend command API into a state-passing one.	Pierre-Marie Pédrot	2016-05-11
\| * \|	Moving the grammar summary to Pcoq.	Pierre-Marie Pédrot	2016-05-11
\| * \|	Delimiting the use of unsafe code in Pcoq.	Pierre-Marie Pédrot	2016-05-10
\| * \|	Overlooked use of Gram instead of G module in Pcoq.	Pierre-Marie Pédrot	2016-05-10
\| * \|	Further tidying of the constr extension code.	Pierre-Marie Pédrot	2016-05-10
\| * \|	Type-safe constr notations.	Pierre-Marie Pédrot	2016-05-10
\| * \|	AlistNsep token now accepts an arbitrary separator.	Pierre-Marie Pédrot	2016-05-10