coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\| *	Fix the API of the new pf_constr_of_global.	Pierre-Marie Pédrot	2017-04-24
\| *	Removing the tclWEAK_PROGRESS tactical.	Pierre-Marie Pédrot	2017-04-24
\| *	Removing the tclNOTSAMEGOAL primitive from the API.	Pierre-Marie Pédrot	2017-04-24
\|/
*	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
*	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\
* \|	Removing most nf_enter in tactics.	Pierre-Marie Pédrot	2017-02-14
* \|	Do not ask for a normalized goal to get hypotheses and conclusions.	Pierre-Marie Pédrot	2017-02-14
* \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing compatibility layers from Tacticals	Pierre-Marie Pédrot	2017-02-14
* \|	Cleaning up interfaces.	Pierre-Marie Pédrot	2017-02-14
* \|	Elim API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Tacticals API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Proofview: tclINDEPENDENTL	Enrico Tassi	2017-02-10
\|/
*	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot	2016-09-15
*	Goal selectors are now tacticals and can be used as such.	Cyprien Mangin	2016-06-14
*	Tacticals: typo in a comment	Pierre Letouzey	2016-02-16
*	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
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Tentative API fix for tactic arguments to be fed to tclWITHHOLES.	Pierre-Marie Pédrot	2015-12-27
\|/ /
* /	Indexing Proofview.goals with a stage.	Pierre-Marie Pédrot	2015-10-20
\|/
*	More expressive API for tclWITHHOLES.	Pierre-Marie Pédrot	2015-02-10
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Update headers.	Maxime Dénès	2015-01-12
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Add Ltac syntax for the [tclIFCATCH] primitive.	Arnaud Spiwack	2014-12-12
*	Constructor tactics backtracking is done using [Tacticals.New] rather than [P...	Arnaud Spiwack	2014-12-08
*	Adding locations to tclZEROMSG.	Pierre-Marie Pédrot	2014-11-20
*	Lazy interpretation of patterns so that expressions such as "intros H H'/H"	Hugo Herbelin	2014-08-18
*	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin	2014-08-18
*	Reorganisation of intropattern code	Hugo Herbelin	2014-08-18
*	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin	2014-07-13
*	Revert "time tac" (committed by mistake).	Hugo Herbelin	2014-07-07
*	time tac	Hugo Herbelin	2014-07-07
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	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
*	Removing the Change_evar refiner rule.	Pierre-Marie Pédrot	2014-03-31
*	Removing tactic compatibility layer from Eqdecide.	Pierre-Marie Pédrot	2014-03-27