coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Moving Refine to its proper module.	Pierre-Marie Pédrot	2016-03-20
*	FIX: of my previous merging mistake	Matej Kosik	2016-02-18
*	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
*	New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).	Hugo Herbelin	2016-01-21
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
* \|	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin	2016-01-21
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \|	Removing the evar_map argument from s_enter.	Pierre-Marie Pédrot	2015-10-29
* \|	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
* \|	Type delayed_open_constr is now monotonic.	Pierre-Marie Pédrot	2015-10-19
* \|	Removing tclEVARS in various places.	Pierre-Marie Pédrot	2015-10-19
* \|	Constraining refine to monotonic functions.	Pierre-Marie Pédrot	2015-10-18
\|/
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Global.env chasing in Inv.	Pierre-Marie Pédrot	2014-11-20
*	Proofview: split [V82] module into [Unsafe] and [V82].	Arnaud Spiwack	2014-10-22
*	Seeing IntroWildcard as an action intro pattern rather than as a naming pattern	Hugo Herbelin	2014-09-30
*	Other bugs with "inversion as" (collision between user-provided names and gen...	Hugo Herbelin	2014-09-11
*	Fixing inversion after having fixed intros_replacing	Hugo Herbelin	2014-09-10
*	A better check that an "as" clause has been given to inversion, so	Hugo Herbelin	2014-09-07
*	Fixing "simple inversion as" (bug #2164).	Hugo Herbelin	2014-09-07
*	Dead code in inv.ml.	Hugo Herbelin	2014-09-07
*	Renaming goal-entering functions.	Pierre-Marie Pédrot	2014-09-06
*	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin	2014-08-18
*	A reorganization of the "assert" tactics (hopefully uniform naming	Hugo Herbelin	2014-08-18
*	Reorganisation of intropattern code	Hugo Herbelin	2014-08-18
*	In Hipattern: some functions not working modulo evar instantiation.	Arnaud Spiwack	2014-08-07
*	Experimentally adding an option for automatically erasing an	Hugo Herbelin	2014-08-05
*	Fix program cases and inversion tactic to correctly record universe constraints.	Matthieu Sozeau	2014-06-24
*	Add an e_type_of to avoid losing universe constraints.	Matthieu Sozeau	2014-06-20
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Giving true proof-terms in inversion instead of metas.	Pierre-Marie Pédrot	2014-04-27
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	Using the new monad tactic in Inv.	Pierre-Marie Pédrot	2014-04-22
*	Removing tactic compatibility layer from Elim.	Pierre-Marie Pédrot	2014-04-22
*	Simplifying interface of elimination tactics. They used dummy clausenvs, and	Pierre-Marie Pédrot	2014-04-22
*	Define Tactics.bring_hyps in the new monad.	Pierre-Marie Pédrot	2014-03-28
*	Removing Tacmach compatibility layer in Inv.	Pierre-Marie Pédrot	2014-03-26
*	Removing tactic compatibility layer from Inv.	Pierre-Marie Pédrot	2014-03-26
*	Moving some tactic code to the new engine.	Pierre-Marie Pédrot	2014-03-26
*	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack	2014-02-27
*	Fixing dependent inversion. Some exceptions were not caught by the tactic	Pierre-Marie Pédrot	2014-01-28
*	Remove some occurrences of obsolete operators	Stephane Glondu	2013-11-22
*	Less use of the list-based interface for goal-bound tactics.	aspiwack	2013-11-02
*	Tachmach.New is now in Proofview.Goal.enter style.	aspiwack	2013-11-02
*	More Proofview.Goal.enter.	aspiwack	2013-11-02