coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\| *	Hopefully better names to constructors of internal_flag, as discussed	Hugo Herbelin	2015-09-23
\| *	Give a way to control if the decidable-equality schemes are built like	Hugo Herbelin	2015-09-23
\| *	Removing the generalization of the body of inductive schemes from	Hugo Herbelin	2015-09-23
\| *	Fix #3948 Anomaly: unknown constant in Print Assumptions	Maxime Dénès	2015-09-20
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|\\|
\| *	Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on.	Pierre-Marie Pédrot	2015-09-15
\| *	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
* \|	All Program obligations now respect the Shrink Obligation flag.	Pierre-Marie Pédrot	2015-09-08
* \|	Fixing the Shrink Obligations option.	Pierre-Marie Pédrot	2015-09-08
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-06
\|\\|
\| *	Also there's an extra space in the error message.	mlasson	2015-09-03
\| *	Code cleaning in Obligations.	Pierre-Marie Pédrot	2015-08-22