coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Using monotonic types for conversion functions.	Pierre-Marie Pédrot	2016-02-15
*	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
* \| \|	Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.	Pierre-Marie Pédrot	2015-12-28
* \| \|	Factorizing code for untyped constr evaluation.	Pierre-Marie Pédrot	2015-12-27
* \| \|	Tentative API fix for tactic arguments to be fed to tclWITHHOLES.	Pierre-Marie Pédrot	2015-12-27
* \| \|	Changing the toplevel type of the int_or_var generic type to int.	Pierre-Marie Pédrot	2015-12-21
\|/ /
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\\|
\| *	FIx parsing of tactic "simple refine".	Maxime Dénès	2015-12-16
\| *	Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".	Guillaume Melquiond	2015-12-16
\| *	Refine tactic now shelves unifiable holes.	Pierre-Marie Pédrot	2015-12-15
\| *	Changing the order of the goals generated by unshelve.	Pierre-Marie Pédrot	2015-12-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	Fixing parsing of the unshelve tactical.	Pierre-Marie Pédrot	2015-12-09
\| *	Adding an unshelve tactical.	Pierre-Marie Pédrot	2015-12-09
* \|	Removing redundant versions of generalize.	Hugo Herbelin	2015-12-05
* \|	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin	2015-12-05
* \|	Moving three related small half-general half-ad-hoc utility functions	Hugo Herbelin	2015-12-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\\|
\| *	Fix [Polymorphic Hint Rewrite].	Matthieu Sozeau	2015-11-27
* \|	Removing the evar_map argument from s_enter.	Pierre-Marie Pédrot	2015-10-29
* \|	Proofview.Goal.sigma returns an indexed evarmap.	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
* \|	Removing tclEVARS in various places.	Pierre-Marie Pédrot	2015-10-19
* \|	Constraining refine to monotonic functions.	Pierre-Marie Pédrot	2015-10-18
* \|	Clarifying and documenting the UState API.	Pierre-Marie Pédrot	2015-10-17
\|/
*	Univs: refined handling of assumptions	Matthieu Sozeau	2015-10-02
*	Univs: fix evar_map handling in Hint processing.	Matthieu Sozeau	2015-10-02
*	Univs: fix many evar_map initializations and leaks.	Matthieu Sozeau	2015-10-02
*	Hopefully better names to constructors of internal_flag, as discussed	Hugo Herbelin	2015-09-23
*	Fix bug #4159	Matthieu Sozeau	2015-05-27
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Using tclZEROMSG instead of tclZERO in several places.	Pierre-Marie Pédrot	2015-04-23
*	Tactical `progress` compares term up to potentially equalisable universes.	Arnaud Spiwack	2015-04-22
*	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
*	More expressive API for tclWITHHOLES.	Pierre-Marie Pédrot	2015-02-10
*	Revert "Removing spurious tclWITHHOLES."	Pierre-Marie Pédrot	2015-02-10
*	Update headers.	Maxime Dénès	2015-01-12
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.	Hugo Herbelin	2014-12-07
*	Used an evar name based on the local def name in "evar" tactic.	Hugo Herbelin	2014-11-25
*	new: Optimize Proof, Optimize Heap	Enrico Tassi	2014-11-09
*	Removing the legacy intro tactic code.	Pierre-Marie Pédrot	2014-11-07
*	Change reduction_of_red_expr to return an e_reduction_function returning	Matthieu Sozeau	2014-10-24
*	Proofview: split [V82] module into [Unsafe] and [V82].	Arnaud Spiwack	2014-10-22
*	Remove the deprecated open-constr based refine.	Arnaud Spiwack	2014-10-22
*	Proofview.Refine: remove the handle type, and simplify the API.	Arnaud Spiwack	2014-10-16