coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Porting type interpretation in Tacinterp to the new tactics.	Pierre-Marie Pédrot	2013-12-02
*	Writing [cut] tactic using the new monad.	Pierre-Marie Pédrot	2013-12-02
*	Removing RefArgType generic argument.	Pierre-Marie Pédrot	2013-12-01
*	Getting rid of casted_open_constr. It was only used by the	Pierre-Marie Pédrot	2013-11-30
*	Adding the necessary hooks to handle tactics in terms.	Pierre-Marie Pédrot	2013-11-27
*	Do not use ugly Dyn features in the Quote plugin. Use instead the	Pierre-Marie Pédrot	2013-11-26
*	Remove the Hiddentac module.	Arnaud Spiwack	2013-11-25
*	Tacinterp: fewer use of old-style goals.	Arnaud Spiwack	2013-11-25
*	Remove some occurrences of obsolete operators	Stephane Glondu	2013-11-22
*	Changes the semantics of Ltac's non-lazy pattern matching in presence of mult...	aspiwack	2013-11-14
*	Implementation of Ltac's match and match goal fully based on IStream.	aspiwack	2013-11-14
*	Remove some dead code in tacinterp.	aspiwack	2013-11-14
*	Do not print tactic notation names at each interpretation step.	ppedrot	2013-11-12
*	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
*	Porting Tactics.assumption to the new engine.	ppedrot	2013-11-08
*	Fix ltac's progress tactical: requires progress in each goal.	aspiwack	2013-11-04
*	Fix change: nf_evar prior to tactic interpretation.	aspiwack	2013-11-04
*	Fix set: nf_evar prior to tactic interpretation.	aspiwack	2013-11-02
*	Plug back infoH.	aspiwack	2013-11-02
*	Plugs back external tactics.	aspiwack	2013-11-02
*	Update comments.	aspiwack	2013-11-02
*	Fix destruct: nf_evar prior to tactic interpretation.	aspiwack	2013-11-02
*	A tactic shelve_unifiable.	aspiwack	2013-11-02
*	Made multiple-goal tactic work after all: .	aspiwack	2013-11-02
*	Make multiple-goal tactics possible after a tclTHEN.	aspiwack	2013-11-02
*	Adds an experimental exactly_once tactical.	aspiwack	2013-11-02
*	Made Proofview.Goal.hyps a named_context.	aspiwack	2013-11-02
*	Adds a tactical once.	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
*	Added the tactical "tac1 + tac2".	aspiwack	2013-11-02
*	Try to remove intermediate allocations when dealing with goal-specific tactics.	aspiwack	2013-11-02
*	Various rewriting, mostly for speed purposes.	aspiwack	2013-11-02
*	Makes the Ltac debugger usable again.	aspiwack	2013-11-02
*	Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).	aspiwack	2013-11-02
*	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack	2013-11-02
*	Bases tactics on an IO monad.	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
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05
*	Actually using the domain function for maps.	ppedrot	2013-08-25
*	get rid of closures in global/proof state	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Small fix in IStream interface.	ppedrot	2013-08-08
*	Small cleaning of printing coercion failures in Ltac interpretation.	ppedrot	2013-08-04