coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\
\| *	Proof using: do not clear unused section hyps automatically	Enrico Tassi	2015-12-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-15
\|\\|
\| *	Univs: Fix bug #4363, nested abstract.	Matthieu Sozeau	2015-12-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	The unshelve tactical now takes future goals into account.	Pierre-Marie Pédrot	2015-12-09
\| *	Adding an unshelve tactical.	Pierre-Marie Pédrot	2015-12-09
* \|	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin	2015-12-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Univs: correctly register universe binders for lemmas.	Matthieu Sozeau	2015-11-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\|
* \|	Inlining the only use of Clenv.connect_clenv.	Pierre-Marie Pédrot	2015-11-18
\| *	Performance fix for destruct.	Pierre-Marie Pédrot	2015-11-17
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-15
\|\\|
\| *	Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.	Pierre-Marie Pédrot	2015-11-12
* \|	Implementing assert and cut with LetIn rather than using a beta-redex.	Hugo Herbelin	2015-11-07
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusion	Matthieu Sozeau	2015-11-04
\| *	Made that the syntax [id]:tac also applies to the shelve, which is after all ...	Hugo Herbelin	2015-11-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-30
\|\\|
\| *	Handle side-effects of Vernacular commands inside proofs better, so that	Matthieu Sozeau	2015-10-29
* \|	Removing the evar_map argument from s_enter.	Pierre-Marie Pédrot	2015-10-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-26
\|\\|
\| *	Fixed (and changed) infoH.	Pierre Courtieu	2015-10-21
* \|	Proofview.Goal.sigma returns an indexed evarmap.	Pierre-Marie Pédrot	2015-10-20
* \|	Indexing Proofview.goals with a stage.	Pierre-Marie Pédrot	2015-10-20
* \|	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot	2015-10-20
* \|	Renaming Goal.enter field into s_enter.	Pierre-Marie Pédrot	2015-10-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
\| *	Categorizing debug messages as such + NonLogical uses loggers.	Pierre Courtieu	2015-10-19
* \|	Adding a monotonic variant of Goal.enter and Goal.nf_enter.	Pierre-Marie Pédrot	2015-10-19
* \|	Making Evarutil.new_evar monotonous.	Pierre-Marie Pédrot	2015-10-18
* \|	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
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-10-16
\|\\|
\| *	Fix #4346 1/2: native casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Fix LemmaOverloading	Matthieu Sozeau	2015-10-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Remove misleading warning (Close #4365)	Enrico Tassi	2015-10-09
\| *	Proof using: let-in policy, optional auto-clear, forward closure*	Enrico Tassi	2015-10-08
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-06
\|\\|
\| *	Fixing emacs output in debugging mode.	Pierre Courtieu	2015-10-06
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\ \
\| \| *	Univs: fix handling of evd's universes and side effects in build_by_tactic	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix handling of side effects/delayed proofs	Matthieu Sozeau	2015-10-02
\| \|/