coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Moving Dnet-related code to tactics/.	Pierre-Marie Pédrot	2014-05-08
*	Removing Termdn, and putting the relevant code in Btermdn. The current Termdn	Pierre-Marie Pédrot	2014-03-03
*	Remove the Hiddentac module.	Arnaud Spiwack	2013-11-25
*	Implementation of Ltac's match and match goal fully based on IStream.	aspiwack	2013-11-14
*	Centralizing the Ltac-defining functions in Tacenv.	ppedrot	2013-11-10
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-10
*	Revert the previous commit. It broke Coq compilation.	ppedrot	2013-11-09
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-09
*	A whole new implemenation of the refine tactic.	aspiwack	2013-11-02
*	Splitted up Genarg in four different levels:	ppedrot	2013-06-21
*	Moving coercion functions out of Tacinterp.	ppedrot	2013-06-12
*	Removing unused module Nbtermdn.	ppedrot	2013-05-09
*	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey	2012-10-16
*	No need to have Refine amongst Hightactics.cm*a	letouzey	2012-05-29
*	Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconcl	letouzey	2012-03-30
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Add a generic tactic option builder. Use it in firstorder to set the	msozeau	2010-03-05
*	Made the side-conditions of lemmas always come last when chaining "apply in"	herbelin	2009-12-13
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Fixing bug #2308 ("instantiate" tactic did not comply with	herbelin	2009-04-24
*	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey	2009-03-20