coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \|	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
\| * \| \|	Simpler data structure for Arules token.	Pierre-Marie Pédrot	2016-05-10
\| * \| \|	Purer implementation of empty level registering in Pcoq.	Pierre-Marie Pédrot	2016-05-10
\| * \| \|	Removing the Entry module now that rules need not be marshalled.	Pierre-Marie Pédrot	2016-05-10
\| * \| \|	Hardening the obsolete unsafe_grammar_statement API.	Pierre-Marie Pédrot	2016-05-10