aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Vernac classification: allow for commands which start proofs but must be sync...Gravatar Arnaud Spiwack2013-12-04
* Porting type interpretation in Tacinterp to the new tactics.Gravatar Pierre-Marie Pédrot2013-12-02
* Writing [cut] tactic using the new monad.Gravatar Pierre-Marie Pédrot2013-12-02
* Removing RefArgType generic argument.Gravatar Pierre-Marie Pédrot2013-12-01
* Ensuring the right parsing of glob arguments, used by refineGravatar Pierre-Marie Pédrot2013-12-01
* Fixing ltac constr variable handling in refine.Gravatar Pierre-Marie Pédrot2013-11-30
* Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
* Fixing abstract tactic by using a dummy name out of a declared proof.Gravatar Pierre-Marie Pédrot2013-11-27
* Adding the necessary hooks to handle tactics in terms.Gravatar Pierre-Marie Pédrot2013-11-27
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Do not use ugly Dyn features in the Quote plugin. Use instead theGravatar Pierre-Marie Pédrot2013-11-26
* Remove the Hiddentac module.Gravatar Arnaud Spiwack2013-11-25
* Tacinterp: fewer use of old-style goals.Gravatar Arnaud Spiwack2013-11-25
* Remove some occurrences of obsolete operatorsGravatar Stephane Glondu2013-11-22
* Using hashes instead of strings in dynamic tags. In case of collision, anGravatar Pierre-Marie Pédrot2013-11-22
* Optimization: in case of empty substitution, merging is trivial.Gravatar Pierre-Marie Pédrot2013-11-19
* Slightly faster version of merging substitutions in TacticMatching.Gravatar ppedrot2013-11-16
* Changes the semantics of Ltac's non-lazy pattern matching in presence of mult...Gravatar aspiwack2013-11-14
* Implementation of Ltac's match and match goal fully based on IStream.Gravatar aspiwack2013-11-14
* Remove some dead code in tacinterp.Gravatar aspiwack2013-11-14
* Do not print tactic notation names at each interpretation step.Gravatar ppedrot2013-11-12
* Centralizing the Ltac-defining functions in Tacenv.Gravatar ppedrot2013-11-10
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-10
* Revert the previous commit. It broke Coq compilation.Gravatar ppedrot2013-11-09
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-09
* Porting Tactics.assumption to the new engine.Gravatar ppedrot2013-11-08
* Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was sol...Gravatar aspiwack2013-11-04
* Fix ltac's progress tactical: requires progress in each goal.Gravatar aspiwack2013-11-04
* Fix the tactical ; [ … ] : the "incorrect number of goal" error was not cau...Gravatar aspiwack2013-11-04
* Fix change: nf_evar prior to tactic interpretation.Gravatar aspiwack2013-11-04
* Allowing proofs starting with a non-empty evarmap.Gravatar ppedrot2013-11-04
* Fixing CAMLP4 compilation.Gravatar ppedrot2013-11-02
* Fix set: nf_evar prior to tactic interpretation.Gravatar aspiwack2013-11-02
* Plug back infoH.Gravatar aspiwack2013-11-02
* Plugs back external tactics.Gravatar aspiwack2013-11-02
* Fix the log of debug auto.Gravatar aspiwack2013-11-02
* Update comments.Gravatar aspiwack2013-11-02
* Doc: solve the bad interaction between Declare Implicit Tactic and refine.Gravatar aspiwack2013-11-02
* The repeat tactic now honors failure levels in ltac.Gravatar aspiwack2013-11-02
* Fix destruct: nf_evar prior to tactic interpretation.Gravatar aspiwack2013-11-02
* Tacticals.New.tclWITHHOLES: clean up.Gravatar aspiwack2013-11-02
* Refine now does iota reduction in addition to beta.Gravatar aspiwack2013-11-02
* Refine: Tactics.New.refine does beta-reduction.Gravatar aspiwack2013-11-02
* Adds a tactic give_up.Gravatar aspiwack2013-11-02
* A tactic shelve_unifiable.Gravatar aspiwack2013-11-02
* Made multiple-goal tactic work after all: .Gravatar aspiwack2013-11-02
* Make multiple-goal tactics possible after a tclTHEN.Gravatar aspiwack2013-11-02
* Adds a shelve tactic.Gravatar aspiwack2013-11-02
* Adds an experimental exactly_once tactical.Gravatar aspiwack2013-11-02
* Made Proofview.Goal.hyps a named_context.Gravatar aspiwack2013-11-02