coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \| \|	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
\| * \| \| \|	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