coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Removing Exc_located and using the new exception enrichement	ppedrot	2013-02-18
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Modulification of identifier	ppedrot	2012-12-14
*	Finish patch for Hint Resolve, stopping to generate new constant names for	msozeau	2012-12-08
*	Monomorphization (tactics)	ppedrot	2012-11-25
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Continue killing hidden tactics : no more generated h_xxx	letouzey	2012-10-15
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Updating headers.	herbelin	2012-08-08