coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	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
\| \| * \|	Fix bug #4705: coqtop accepts both -emacs and -ideslave.	Pierre-Marie Pédrot	2016-05-03
* \| \| \|	setup.txt : a guide explaining taming Emacs, Merlin, Company, Ocamldebug.	Matej Kosik	2016-05-03
\| \| * \|	Call hooks when terminating a definition proof (bug #4663).	Guillaume Melquiond	2016-05-03
\| \| * \|	Remove extraneous space in coqtop/pg output (bug #4675).	Guillaume Melquiond	2016-05-03
\| \| * \|	Make votour a bit more robust/forgiving with respect to user commands (bug #4...	Guillaume Melquiond	2016-05-02
\| \| * \|	Properly handle notations containing spaces (bug #4538).	Guillaume Melquiond	2016-05-02
\| \| * \|	Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).	Guillaume Melquiond	2016-05-02
* \| \| \|	Generate parsing rules for ML tactics in the same order as before a7917a32.	Pierre-Marie Pédrot	2016-05-02
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-02
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
* \| \| \|	Useless code in Tacentries.	Pierre-Marie Pédrot	2016-05-02
\| * \| \|	Reduce ide/coq.png to 256x256.	Guillaume Melquiond	2016-04-29
\| * \| \|	Fix incorrect cbv reduction of primitive projections. (Bug #4634)	Guillaume Melquiond	2016-04-29
\| * \| \|	Make the language grammar much more precise. (Fix bugs #4682 and #4683)	Guillaume Melquiond	2016-04-28
\| * \| \|	Update tutorial (fix bug #4699).	Guillaume Melquiond	2016-04-28
\| * \| \|	Fix missing newline in coqchk engagement (bug #4694).	Guillaume Melquiond	2016-04-28
\| * \| \|	An example for cd139311e, showing a consequence of not converting	Hugo Herbelin	2016-04-28
* \| \| \|	Revert "A heuristic to add parentheses in the presence of rules such as"	Hugo Herbelin	2016-04-27