aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2014-02-25Tacinterp: remove the is_value check in Ltac's let-in.Arnaud Spiwack
2014-02-25Tacinterp: fewer enterl still.Arnaud Spiwack
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-24TacticMatching: avoid some closure allocation in (<*>).Arnaud Spiwack
2014-02-24Removed some trailing whitespaces.Arnaud Spiwack
2014-02-24IStream: a concat_map primitive.Arnaud Spiwack
2014-02-24A view type for IStream.Arnaud Spiwack
2014-02-16Removing non-marshallable data from the Agram constructor. Instead ofPierre-Marie Pédrot
2014-02-04The constructor tactic now returns several successes.Pierre-Marie Pédrot
2014-02-02Fixing bug #3226.Pierre-Marie Pédrot
2014-01-31In Ltac's exact tactic: avoid checking the type of the term twice.Arnaud Spiwack
2014-01-28Fixing dependent inversion. Some exceptions were not caught by the tacticPierre-Marie Pédrot
2014-01-19Adding a default object to generic argument registering mechanism.Pierre-Marie Pédrot
2014-01-17Fixing bug #1758: Print Hint output can be misleading if variable shadows hyp...Pierre-Marie Pédrot
2014-01-14Removing unused tactics in rewrite.Pierre-Marie Pédrot
2014-01-10Exporting the full pretyper options in Goal.constr_of_raw.Pierre-Marie Pédrot
2014-01-10Fix bug#2080: error message on Ltac name clash with primitive tacticsxclerc
2014-01-06Algebraized "No such hypothesis" errorsPierre-Marie Pédrot
2014-01-04Code cleaning in Rewrite, may also result faster.Pierre-Marie Pédrot
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-12-24Simplifying the use of hypinfos in Rewrite.Pierre-Marie Pédrot
2013-12-23Rewrite.ml: removing direction flag from hypinfo.Pierre-Marie Pédrot
2013-12-22Do not pass unification flags around in Rewrite.Pierre-Marie Pédrot
2013-12-22Slight code cleaning ensuring more static invariants in Rewrite.Pierre-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-16Get rid of messages "emitting ..." when compiling .v filesPierre Letouzey
2013-12-16Dedicated inductive for return values of rewrite strategies.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-04Vernac classification: allow for commands which start proofs but must be sync...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-12-01Ensuring the right parsing of glob arguments, used by refinePierre-Marie Pédrot
2013-11-30Fixing ltac constr variable handling in refine.Pierre-Marie Pédrot
2013-11-30Getting rid of casted_open_constr. It was only used by thePierre-Marie Pédrot
2013-11-27Fixing abstract tactic by using a dummy name out of a declared proof.Pierre-Marie Pédrot
2013-11-27Adding the necessary hooks to handle tactics in terms.Pierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 18:28:15 +0000