coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Moving Proofview to pretyping/.	Pierre-Marie Pédrot	2016-03-20
*	Moving Refine to its proper module.	Pierre-Marie Pédrot	2016-03-20
*	Making Proofview independent of Logic.	Pierre-Marie Pédrot	2016-03-20
*	Extruding the code for the Existential command from Proofview.	Pierre-Marie Pédrot	2016-03-20
*	Fix the comment of Refine.refine	Matthieu Sozeau	2016-03-14
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Use streams rather than strings to handle bullet suggestions.	Guillaume Melquiond	2016-01-02
\|/ /
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	Adding an unshelve tactical.	Pierre-Marie Pédrot	2015-12-09
* \|	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
* \|	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
* \|	Adding a monotonic variant of Goal.enter and Goal.nf_enter.	Pierre-Marie Pédrot	2015-10-19
* \|	Constraining refine to monotonic functions.	Pierre-Marie Pédrot	2015-10-18
* \|	Exposing the minimal amount of internal of the Logic monad in order to	Pierre-Marie Pédrot	2015-05-06
\|/
*	Fix some typos in comments.	Guillaume Melquiond	2015-02-23
*	Update headers.	Maxime Dénès	2015-01-12
*	Fixed and extend bullet related info/error messages. + doc.	Pierre Courtieu	2015-01-08
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Make sure the goals on the shelve are identified as goal and unresolvable for...	Arnaud Spiwack	2014-12-12
*	Exporting store of goals so that new_evar in convert, intro, etc. can	Hugo Herbelin	2014-12-07
*	Adding missing unsafe primitives to Proofview.	Pierre-Marie Pédrot	2014-11-30
*	new: Optimize Proof, Optimize Heap	Enrico Tassi	2014-11-09
*	Info: do not record info trace unless needed.	Arnaud Spiwack	2014-11-01
*	Info: print a name for the primitive tactics in [Proofview].	Arnaud Spiwack	2014-11-01
*	Add [Info] command.	Arnaud Spiwack	2014-11-01
*	An API for info traces.	Arnaud Spiwack	2014-11-01
*	Specializing tclBREAK so that it can choose the return exception in case	Pierre-Marie Pédrot	2014-10-22
*	Proofview: documentation and re-ordering.	Arnaud Spiwack	2014-10-22
*	Split [Proofview] into a file where the basic operations on the state are def...	Arnaud Spiwack	2014-10-22
*	Make names in [Proofview_monad] more uniform.	Arnaud Spiwack	2014-10-22
*	Proofview: move [list_goto] to the [CList] module.	Arnaud Spiwack	2014-10-22
*	Proofview: remove a redundant primitive.	Arnaud Spiwack	2014-10-22
*	Proofview: move more functions to the Unsafe module.	Arnaud Spiwack	2014-10-22
*	Proofview: split [V82] module into [Unsafe] and [V82].	Arnaud Spiwack	2014-10-22
*	Proofview.mli: no more reference to Goal.goal.	Arnaud Spiwack	2014-10-22
*	Remove unused functions for side effects.	Arnaud Spiwack	2014-10-22
*	Refactoring proofview: make the definition of the logic monad polymorphic.	Arnaud Spiwack	2014-10-16
*	Put evars remaining after a tactic on the shelf.	Arnaud Spiwack	2014-10-16
*	Proofview: remove unused [refresh_sigma] compatibility primitive.	Arnaud Spiwack	2014-10-16
*	Expose Proofview.Refine.with_type in the API.	Arnaud Spiwack	2014-10-16
*	Proofview.Refine: remove the handle type, and simplify the API.	Arnaud Spiwack	2014-10-16
*	Adding a tactic which fails if one of the goals under focus is dependent in a...	Hugo Herbelin	2014-10-13