coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Vernac classification: allow for commands which start proofs but must be sync...	Arnaud Spiwack	2013-12-04
*	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
*	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
*	Fixing abstract tactic by using a dummy name out of a declared proof.	Pierre-Marie Pédrot	2013-11-27
*	Adding the necessary hooks to handle tactics in terms.	Pierre-Marie Pédrot	2013-11-27
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	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
*	Using hashes instead of strings in dynamic tags. In case of collision, an	Pierre-Marie Pédrot	2013-11-22
*	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