coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Type-safe Egramml.grammar_prod_item.	Pierre-Marie Pédrot	2015-10-27
*	Finer type for Pcoq.interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
*	Indexing existentially quantified entries returned by interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-26
\|\
\| *	Minor module cleanup : error HigherOrderInclude was never happening	Pierre Letouzey	2015-10-25
* \|	Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.	Pierre-Marie Pédrot	2015-10-21
* \|	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot	2015-10-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
* \|	Constraining refine to monotonic functions.	Pierre-Marie Pédrot	2015-10-18
\| *	Miscellaneous typos, spacing, US spelling in comments or variable names.	Hugo Herbelin	2015-10-18
* \|	Clarifying and documenting the UState API.	Pierre-Marie Pédrot	2015-10-17
\| *	Lemmas accept the Local flag.	Pierre-Marie Pédrot	2015-10-17
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Remove -vm flag of coqtop.	Maxime Dénès	2015-10-14
\| *	Fixing bug #4367: Wrong error message in unification.	Pierre-Marie Pédrot	2015-10-14
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-12
\|\\|
\| *	Fix Definition id := Eval <redexpr> in by passing the right universe	Matthieu Sozeau	2015-10-12
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-10
\|\\|
\| *	Code cleaning in VM (with Benjamin).	Maxime Dénès	2015-10-09
\| *	Fix Next Obligation to not raise an anomaly in case of mutual	Matthieu Sozeau	2015-10-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Axioms now support the universe binding syntax.	Pierre-Marie Pédrot	2015-10-08
\| *	aux_file: export API to ease writing of a Proof Using annotator.	Enrico Tassi	2015-10-08
\| *	Proof using: let-in policy, optional auto-clear, forward closure*	Enrico Tassi	2015-10-08
\| *	Spawn: use each socket exclusively for writing or reading	Enrico Tassi	2015-10-08
\| *	Goptions: new value type: optional string	Enrico Tassi	2015-10-08
\| *	Univs: fix FingerTree contrib.	Matthieu Sozeau	2015-10-07
\| *	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
* \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-06
\|\\|
\| *	Univs: fix handling of evar_map in identity coercion construction.	Matthieu Sozeau	2015-10-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\ \
\| \| *	Fix after rebase...	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix inference of the lowest sort for records.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: correcly compute the levels of records when they fall in Prop.	Matthieu Sozeau	2015-10-02
\| \| *	Univs/program: handle side effects in obligations.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix Show Universes.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix environment handling in scheme building.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix after rebase (from_ctx/from_env)	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix many evar_map initializations and leaks.	Matthieu Sozeau	2015-10-02
\| \| *	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau	2015-10-02
\| \|/
\| *	Prevent States.intern_state and System.extern_intern from looking up files in...	Guillaume Melquiond	2015-09-29
\| *	Remove some uses of Loadpath.get_paths.	Guillaume Melquiond	2015-09-29
\| *	Make -load-vernac-object respect the loadpath.	Guillaume Melquiond	2015-09-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-25
\|\\|
\| *	The -require option now accepts a logical path instead of a physical one.	Pierre-Marie Pédrot	2015-09-25
\| *	Updating the documentation and the toolchain w.r.t. the change in -compile.	Pierre-Marie Pédrot	2015-09-25
\| *	The -compile option now accepts ".v" files and outputs a warning otherwise.	Pierre-Marie Pédrot	2015-09-25