coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Optimization: in case of empty substitution, merging is trivial.	Pierre-Marie Pédrot	2013-11-19
*	Slightly faster version of merging substitutions in TacticMatching.	ppedrot	2013-11-16
*	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 Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was sol...	aspiwack	2013-11-04
*	Fix ltac's progress tactical: requires progress in each goal.	aspiwack	2013-11-04
*	Fix the tactical ; [ … ] : the "incorrect number of goal" error was not cau...	aspiwack	2013-11-04
*	Fix change: nf_evar prior to tactic interpretation.	aspiwack	2013-11-04
*	Allowing proofs starting with a non-empty evarmap.	ppedrot	2013-11-04
*	Fixing CAMLP4 compilation.	ppedrot	2013-11-02
*	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
*	Fix the log of debug auto.	aspiwack	2013-11-02
*	Update comments.	aspiwack	2013-11-02
*	Doc: solve the bad interaction between Declare Implicit Tactic and refine.	aspiwack	2013-11-02
*	The repeat tactic now honors failure levels in ltac.	aspiwack	2013-11-02
*	Fix destruct: nf_evar prior to tactic interpretation.	aspiwack	2013-11-02
*	Tacticals.New.tclWITHHOLES: clean up.	aspiwack	2013-11-02
*	Refine now does iota reduction in addition to beta.	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
*	Made multiple-goal tactic work after all: .	aspiwack	2013-11-02
*	Make multiple-goal tactics possible after a tclTHEN.	aspiwack	2013-11-02
*	Adds a shelve tactic.	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
*	Refine does beta-reductions.	aspiwack	2013-11-02
*	Adds a tactical once.	aspiwack	2013-11-02
*	Corrects the semantics of the "+" tactical.	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
*	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
*	Fix behaviour of the refine tactic with respect to evars in types.	aspiwack	2013-11-02
*	Makes the Ltac debugger usable again.	aspiwack	2013-11-02
*	Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...	aspiwack	2013-11-02
*	Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).	aspiwack	2013-11-02
*	Clean up a warning.	aspiwack	2013-11-02
*	The tactic [admit] exits with the "unsafe" status.	aspiwack	2013-11-02