aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Fixing dependent inversion. Some exceptions were not caught by the tacticGravatar Pierre-Marie Pédrot2014-01-28
* Adding a default object to generic argument registering mechanism.Gravatar Pierre-Marie Pédrot2014-01-19
* Fixing bug #1758: Print Hint output can be misleading if variable shadows hyp...Gravatar Pierre-Marie Pédrot2014-01-17
* Removing unused tactics in rewrite.Gravatar Pierre-Marie Pédrot2014-01-14
* Exporting the full pretyper options in Goal.constr_of_raw.Gravatar Pierre-Marie Pédrot2014-01-10
* Fix bug#2080: error message on Ltac name clash with primitive tacticsGravatar xclerc2014-01-10
* Algebraized "No such hypothesis" errorsGravatar Pierre-Marie Pédrot2014-01-06
* Code cleaning in Rewrite, may also result faster.Gravatar Pierre-Marie Pédrot2014-01-04
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* Simplifying the use of hypinfos in Rewrite.Gravatar Pierre-Marie Pédrot2013-12-24
* Rewrite.ml: removing direction flag from hypinfo.Gravatar Pierre-Marie Pédrot2013-12-23
* Do not pass unification flags around in Rewrite.Gravatar Pierre-Marie Pédrot2013-12-22
* Slight code cleaning ensuring more static invariants in Rewrite.Gravatar Pierre-Marie Pédrot2013-12-22
* Notations now accept the $(...)$ tactic-in-term syntax. They are resolved atGravatar Pierre-Marie Pédrot2013-12-22
* Removing the useless pattern ident genarg.Gravatar Pierre-Marie Pédrot2013-12-19
* Using interp_genarg in tactic notations where possible, instead of an ad-hocGravatar Pierre-Marie Pédrot2013-12-19
* Bad use of Obj.magic in interpretation of TacAlias arguments.Gravatar Pierre Boutillier2013-12-19
* Printing function for Stdargs in debuggerGravatar Pierre Boutillier2013-12-19
* Removing the need of evarmaps in constr internalization.Gravatar Pierre-Marie Pédrot2013-12-17
* Get rid of messages "emitting ..." when compiling .v filesGravatar Pierre Letouzey2013-12-16
* Dedicated inductive for return values of rewrite strategies.Gravatar Pierre-Marie Pédrot2013-12-16
* Fixing backtrace registering of various tactic-related try-with blocks.Gravatar Pierre-Marie Pédrot2013-12-11
* Stylistic change.Gravatar Arnaud Spiwack2013-12-09
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 08:45:20 +0000