coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \|	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
\| * \|	Removing dead code in Compat.	Pierre-Marie Pédrot	2016-05-10
\|/ /
* \|	Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"	Enrico Tassi	2016-05-10
* \|	STM: code cleanup	Enrico Tassi	2016-05-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-09
\|\\|
\| *	Fix bug #3887: Better error message for "More than one program with unsolved ...	Pierre-Marie Pédrot	2016-05-09
\| *	Rename Lexer -> CLexer.	Pierre-Marie Pédrot	2016-05-09
\| *	Fix typo in configure's option description.	Guillaume Melquiond	2016-05-09
\| *	Use "md5 -q" on FreeBSD architectures (bug #4719).	Guillaume Melquiond	2016-05-09
\| *	Use the actual location of an error in the error pane (bug #4169).	Guillaume Melquiond	2016-05-09
* \|	Exposing structure of the entries to tactic notation printers.	Pierre-Marie Pédrot	2016-05-08
\|\ \
\| * \|	Actually using the symbol information to print Tactic Notations properly.	Pierre-Marie Pédrot	2016-05-08
\| * \|	Removing dead code in Pptactic.	Pierre-Marie Pédrot	2016-05-08
\| * \|	Pass user symbol to tactic notation printers.	Pierre-Marie Pédrot	2016-05-08
\|/ /
* \|	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
* \|	Change the toplevel representation of Ltac values to an untyped one.	Pierre-Marie Pédrot	2016-05-08
\|\ \
\| \| *	Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.	Pierre-Marie Pédrot	2016-05-08
\| * \|	Normalizing the names of dynamic types to follow a typ_* scheme.	Pierre-Marie Pédrot	2016-05-04
\| \| *	typo	Enrico Tassi	2016-05-04
\| \| *	NPeano : improve compatibility for this deprecated file via compat notations	Pierre Letouzey	2016-05-04
\| * \|	Removing useless generic arguments.	Pierre-Marie Pédrot	2016-05-04
\| * \|	Interpretation function can return any untyped value.	Pierre-Marie Pédrot	2016-05-04
\| * \|	Removing external uses of Val.inject and making Geninterp.interp return Val.t	Pierre-Marie Pédrot	2016-05-04
\| * \|	Removing the Value.of_* API for parameterized types.	Pierre-Marie Pédrot	2016-05-04
\| * \|	Do not generate generic arguments for data which only requires toplevel values.	Pierre-Marie Pédrot	2016-05-04
\| * \|	More toplevel value representation sharing.	Pierre-Marie Pédrot	2016-05-04
\| * \|	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
\| * \|	Simplifying the code of Tacinterp.	Pierre-Marie Pédrot	2016-05-04
\| * \|	Getting rid of the Geninterp.generic_interp function.	Pierre-Marie Pédrot	2016-05-04
\| * \|	Switching to an untyped toplevel representation for Ltac values.	Pierre-Marie Pédrot	2016-05-04
\| * \|	Moving Ftactic and Geninterp to the engine folder.	Pierre-Marie Pédrot	2016-05-04
\|/ /
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\\|
\| *	Int.v: simplify Jason's commit 5b4e3ace	Pierre Letouzey	2016-05-04
\| *	Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...	Pierre Letouzey	2016-05-04
\| \|\
\| * \|	Fixing subst.out after changing spacing in goal output (24a125b77).	Hugo Herbelin	2016-05-04
\| * \|	Fix Haskell extraction for terms over 45 characters long	Nickolai Zeldovich	2016-05-04
\| * \|	Handle primitive projections inside types when extracting (bug #4616).	Guillaume Melquiond	2016-05-04
\| * \|	Fix for #4603, part 3: definitions inside proofs not handled properly by coqc.	Maxime Dénès	2016-05-04
* \| \|	Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into t...	Pierre Letouzey	2016-05-04
\|\ \ \
\| \| * \|	Increase the size of the dumpglob buffer for cooking notations (bug #4708).	Guillaume Melquiond	2016-05-04
\| \| * \|	In Regular Subst Tactic mode, ensure that the order of hypotheses is	Hugo Herbelin	2016-05-03
\| \| * \|	Fix bug #4707: clearbody much slower in 8.5pl1.	Pierre-Marie Pédrot	2016-05-03
\| \| * \|	Fix bug #3825: Universe annotations on notations should pass through or be re...	Pierre-Marie Pédrot	2016-05-03
\| \| * \|	Test file for #4695: Slow Qed.	Maxime Dénès	2016-05-03
\| \| * \|	Fix bug #4292: Unexpected functor objects.	Pierre-Marie Pédrot	2016-05-03
\| \| * \|	Use the canonical name when looking for an eliminator (bug #4670).	Guillaume Melquiond	2016-05-03
* \| \| \|	A note concerning the "Drop" command.	Matej Kosik	2016-05-03