coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Expliciting some uses of Compat module.	Pierre-Marie Pédrot	2015-10-21
\| *	Bug #3956 is fixed.	Matthieu Sozeau	2015-10-21
* \|	Removing test for bug #3956.	Pierre-Marie Pédrot	2015-10-21
\| *	Fixed (and changed) infoH.	Pierre Courtieu	2015-10-21
\| *	Fix lemma-overloading	Matthieu Sozeau	2015-10-20
* \|	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
* \|	Expliciting the uses of the old Tacmach API in Tactics.	Pierre-Marie Pédrot	2015-10-19
* \|	Removing some unsafe uses of monotonicity.	Pierre-Marie Pédrot	2015-10-19
\| *	Do occur-check w.r.t existential's types also when instantiating an evar.	Matthieu Sozeau	2015-10-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
* \|	Type delayed_open_constr is now monotonic.	Pierre-Marie Pédrot	2015-10-19
\| *	Categorizing debug messages as such + NonLogical uses loggers.	Pierre Courtieu	2015-10-19
\| *	Test for #4372 (anomaly in inversion in the presence of fake dependency).	Hugo Herbelin	2015-10-19
* \|	More monotonicity in Tactics.	Pierre-Marie Pédrot	2015-10-19
\| *	Turning anomaly into error for #4372 (weakness of inversion in the	Hugo Herbelin	2015-10-19
* \|	Removing tclEVARS in various places.	Pierre-Marie Pédrot	2015-10-19
* \|	Reducing the uses of tclEVARS in Tactics by using monotonous functions.	Pierre-Marie Pédrot	2015-10-19
* \|	Adding a monotonic variant of Goal.enter and Goal.nf_enter.	Pierre-Marie Pédrot	2015-10-19
* \|	Function debug mode more formatted.	Pierre Courtieu	2015-10-19
\| *	Partly fixes #3225. Removed some old experimental stuff in funind.	Pierre Courtieu	2015-10-19
\| *	Fixed #4274, bad formatting of messages in emacs mode.	Pierre Courtieu	2015-10-19
\| *	Documenting the option "Strict Universe Declaration" in CHANGES.	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
\| *	Using "__" rather than this unelegant arbitrary "A" for the name of variables...	Hugo Herbelin	2015-10-18
\| *	Reference Manual: Applying standard style recommendation about not	Hugo Herbelin	2015-10-18
\| *	Fixing #4198 (continued): not matching within the inner lambdas/let-ins	Hugo Herbelin	2015-10-18
\| *	Using appropriate lambda decomposition function counting let-ins when	Hugo Herbelin	2015-10-18
\| *	Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,	Hugo Herbelin	2015-10-18
* \|	Adding a notion of monotonous evarmap.	Pierre-Marie Pédrot	2015-10-18
* \|	Clarifying and documenting the UState API.	Pierre-Marie Pédrot	2015-10-17
* \|	Dedicated file for universe unification context manipulation.	Pierre-Marie Pédrot	2015-10-17
\| *	Lemmas accept the Local flag.	Pierre-Marie Pédrot	2015-10-17
\| *	Test for bug #4325.	Pierre-Marie Pédrot	2015-10-17
\| *	Generalize fix for auto from PMP to eauto and typeclasses eauto.	Matthieu Sozeau	2015-10-16
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-10-16
\|\\|
* \|	Hashcons bytecode generated by the VM.	Pierre-Marie Pédrot	2015-10-16
* \|	Exporting a purely functional interface to bytecode patching.	Pierre-Marie Pédrot	2015-10-16
\| *	Remove left2right reference from the kernel.	Maxime Dénès	2015-10-16
\| *	Merge hint lists instead of appending them. (Fix bug #3199)	Guillaume Melquiond	2015-10-16
\| *	Avoid dependency of the pretyper on C code.	Maxime Dénès	2015-10-15
\| *	Test file for #4346: Set is no longer of type Type	Maxime Dénès	2015-10-15
\| *	Fix #4346 2/2: VM casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
\| *	Fix #4346 1/2: native casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
\| *	Warn user when bytecode compilation fails.	Maxime Dénès	2015-10-15
\| *	Remove now useless exception handler in default conversion.	Maxime Dénès	2015-10-15