coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\| \|/
\| *	Changed status of Info messages from notice to info.	Pierre Courtieu	2015-10-02
* \|	Removing meta_with_name from Evd.	Pierre-Marie Pédrot	2015-09-27
* \|	Removing uselessly duplicated function in Evd.	Pierre-Marie Pédrot	2015-09-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-25
\|\\|
\| *	Removing the generalization of the body of inductive schemes from	Hugo Herbelin	2015-09-23
\| *	Proof: suggest Admitted->Qed only if the proof is really complete (#4349)	Enrico Tassi	2015-09-20
* \|	Fix previous merge.	Maxime Dénès	2015-09-17
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|\\|
\| *	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
* \|	Opacifying the proof_terminator type.	Pierre-Marie Pédrot	2015-09-08
\| *	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
\| *	Removing the generalization of the body of inductive schemes from	Hugo Herbelin	2015-08-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-29
\|\\|
\| *	Fixing what seems to be a typo.	Hugo Herbelin	2015-07-29
\| *	Slightly improving line break formatting in Info command.	Hugo Herbelin	2015-07-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-24
\|\\|
\| *	Fix `Pp` function used by the `Info` command.	Arnaud Spiwack	2015-06-23
* \|	Merge remote-tracking branch 'forge/v8.5'	Pierre Boutillier	2015-06-22
\|\\|
\| *	STM: states coming from workers have no proof terminators (Close #4246)	Enrico Tassi	2015-06-09
\| *	Admitted does not drop poly-univ constraints (Fix #4244)	Enrico Tassi	2015-06-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-01
\|\\|
\| *	STM/Univ: save initial univs (the ones in the statement) in Proof.proof	Enrico Tassi	2015-05-29
\| *	Fix bug #4159	Matthieu Sozeau	2015-05-27
\| *	Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...	Pierre-Marie Pédrot	2015-05-18