aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacinterp.ml
AgeCommit message (Expand)Author
2014-02-25Tacinterp: fewer Proofview.Goal.enterl.Arnaud Spiwack
2014-02-25Tacinterp: clean up.Arnaud Spiwack
2014-02-25Tacinterp: remove unnecessary return/bind pairs.Arnaud Spiwack
2014-02-24A view type for IStream.Arnaud Spiwack
2014-01-31In Ltac's exact tactic: avoid checking the type of the term twice.Arnaud Spiwack
2014-01-06Algebraized "No such hypothesis" errorsPierre-Marie Pédrot
2013-12-22Notations now accept the $(...)$ tactic-in-term syntax. They are resolved atPierre-Marie Pédrot
2013-12-19Removing the useless pattern ident genarg.Pierre-Marie Pédrot
2013-12-19Using interp_genarg in tactic notations where possible, instead of an ad-hocPierre-Marie Pédrot
2013-12-19Bad use of Obj.magic in interpretation of TacAlias arguments.Pierre Boutillier
2013-12-19Printing function for Stdargs in debuggerPierre Boutillier
2013-12-17Removing the need of evarmaps in constr internalization.Pierre-Marie Pédrot
2013-12-11Fixing backtrace registering of various tactic-related try-with blocks.Pierre-Marie Pédrot
2013-12-09Stylistic change.Arnaud Spiwack
2013-12-02Porting type interpretation in Tacinterp to the new tactics.Pierre-Marie Pédrot
2013-12-02Writing [cut] tactic using the new monad.Pierre-Marie Pédrot
2013-12-01Removing RefArgType generic argument.Pierre-Marie Pédrot
2013-11-30Getting rid of casted_open_constr. It was only used by thePierre-Marie Pédrot
2013-11-27Adding the necessary hooks to handle tactics in terms.Pierre-Marie Pédrot
2013-11-26Do not use ugly Dyn features in the Quote plugin. Use instead thePierre-Marie Pédrot
2013-11-25Remove the Hiddentac module.Arnaud Spiwack
2013-11-25Tacinterp: fewer use of old-style goals.Arnaud Spiwack
2013-11-22Remove some occurrences of obsolete operatorsStephane Glondu
2013-11-14Changes the semantics of Ltac's non-lazy pattern matching in presence of mult...aspiwack
2013-11-14Implementation of Ltac's match and match goal fully based on IStream.aspiwack
2013-11-14Remove some dead code in tacinterp.aspiwack
2013-11-12Do not print tactic notation names at each interpretation step.ppedrot
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-09Revert the previous commit. It broke Coq compilation.ppedrot
2013-11-09Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-08Porting Tactics.assumption to the new engine.ppedrot
2013-11-04Fix ltac's progress tactical: requires progress in each goal.aspiwack
2013-11-04Fix change: nf_evar prior to tactic interpretation.aspiwack
2013-11-02Fix set: nf_evar prior to tactic interpretation.aspiwack
2013-11-02Plug back infoH.aspiwack
2013-11-02Plugs back external tactics.aspiwack
2013-11-02Update comments.aspiwack
2013-11-02Fix destruct: nf_evar prior to tactic interpretation.aspiwack
2013-11-02A tactic shelve_unifiable.aspiwack
2013-11-02Made multiple-goal tactic work after all: .aspiwack
2013-11-02Make multiple-goal tactics possible after a tclTHEN.aspiwack
2013-11-02Adds an experimental exactly_once tactical.aspiwack
2013-11-02Made Proofview.Goal.hyps a named_context.aspiwack
2013-11-02Adds a tactical once.aspiwack
2013-11-02Tachmach.New is now in Proofview.Goal.enter style.aspiwack
2013-11-02More Proofview.Goal.enter.aspiwack
2013-11-02Added the tactical "tac1 + tac2".aspiwack
2013-11-02Try to remove intermediate allocations when dealing with goal-specific tactics.aspiwack
2013-11-02Various rewriting, mostly for speed purposes.aspiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 17:15:41 +0000