coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack	2014-08-06
*	Experimentally adding an option for automatically erasing an	Hugo Herbelin	2014-08-05
*	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi	2014-08-05
*	The [refine] tactic now accepts [uconstr].	Arnaud Spiwack	2014-08-05
*	Add [guard] tactic.	Arnaud Spiwack	2014-08-01
*	Add a tactic [swap i j] to swap the position of goals [i] and [j].	Arnaud Spiwack	2014-07-25
*	Adds a cycle tactic to reorder goals in a loop.	Arnaud Spiwack	2014-07-25
*	Moved code for finding subterms (pattern, induction, set, generalize, ...)	Hugo Herbelin	2014-06-28
*	Oops, I fixed the .ml's	Matthieu Sozeau	2014-06-23
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18
*	Removing decompose record / sum from the tactic AST.	Pierre-Marie Pédrot	2014-05-21
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Removing the compatibility layer from Leminv. Also removed an undocumented	Pierre-Marie Pédrot	2014-04-22
*	Closing bug #3260	Julien Forest	2014-04-14
*	Removing the Change_evar refiner rule.	Pierre-Marie Pédrot	2014-03-31
*	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
*	Get rid of the enterl/glist API for Proofview.Goal.	Arnaud Spiwack	2014-02-27
*	Exporting the full pretyper options in Goal.constr_of_raw.	Pierre-Marie Pédrot	2014-01-10
*	Ensuring the right parsing of glob arguments, used by refine	Pierre-Marie Pédrot	2013-12-01
*	Fixing ltac constr variable handling in refine.	Pierre-Marie Pédrot	2013-11-30
*	Getting rid of casted_open_constr. It was only used by the	Pierre-Marie Pédrot	2013-11-30
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	Remove the Hiddentac module.	Arnaud Spiwack	2013-11-25
*	Doc: solve the bad interaction between Declare Implicit Tactic and refine.	aspiwack	2013-11-02
*	Refine: Tactics.New.refine does beta-reduction.	aspiwack	2013-11-02
*	Adds a tactic give_up.	aspiwack	2013-11-02
*	A tactic shelve_unifiable.	aspiwack	2013-11-02
*	Adds a shelve tactic.	aspiwack	2013-11-02
*	Refine does beta-reductions.	aspiwack	2013-11-02
*	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
*	Clean up a warning.	aspiwack	2013-11-02
*	The tactic [admit] exits with the "unsafe" status.	aspiwack	2013-11-02
*	A whole new implemenation of the refine tactic.	aspiwack	2013-11-02
*	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack	2013-11-02
*	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05
*	Vernac classification streamlined (handles VERNAC EXTEND)	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Start documenting new [rewrite_strat] tactic that applies rewriting	msozeau	2013-06-04
*	Making the behavior of "injection ... as ..." more natural:	herbelin	2013-06-02
*	Granting wish #3014:	ppedrot	2013-05-12
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	code simplifications concerning Summary	letouzey	2013-04-22
*	Restrict (try...with...) to avoid catching critical exn (part 13)	letouzey	2013-03-13