aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Removing some compatibility layers in Tactics.Gravatar Pierre-Marie Pédrot2016-05-17
* Removing the old refine tactic from the Tactics module.Gravatar Pierre-Marie Pédrot2016-05-17
* Put the "move" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-17
* Put the "change" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "specialize_eq" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "generalize dependent" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "*_cast_no_check" tactics in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "exact" family of tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "exact_constr" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Normalizing the names of dynamic types to follow a typ_* scheme.Gravatar Pierre-Marie Pédrot2016-05-04
* Removing external uses of Val.inject and making Geninterp.interp return Val.tGravatar Pierre-Marie Pédrot2016-05-04
* Removing the Value.of_* API for parameterized types.Gravatar Pierre-Marie Pédrot2016-05-04
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* Getting rid of the Geninterp.generic_interp function.Gravatar Pierre-Marie Pédrot2016-05-04
* Switching to an untyped toplevel representation for Ltac values.Gravatar Pierre-Marie Pédrot2016-05-04
* Moving Ftactic and Geninterp to the engine folder.Gravatar Pierre-Marie Pédrot2016-05-04
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\
| * In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
| * Fix bug #4707: clearbody much slower in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-05-03
* | Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
* | In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-09
|\|
| * Allow to unset the refinement mode of Instance in MLGravatar Matthieu Sozeau2016-04-07
| * Fixing an incorrect use of prod_appvect on a term which was not aGravatar Hugo Herbelin2016-04-07
| * Fixing the "No applicable tactic" non informative error messageGravatar Hugo Herbelin2016-04-03
* | Moving Autorewrite back to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
* | Moving Eqdecide to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
* | Moving Eauto and Class_tactics to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
* | Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
* | Moving Tacsubst to hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
* | Relying on generic arguments to represent Extern hints.Gravatar Pierre-Marie Pédrot2016-03-20
* | Adding a new Ltac generic argument for forced tactics returing unit.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving Tacenv to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving Tactic_debug to Hightactic.Gravatar Pierre-Marie Pédrot2016-03-20
* | Making Evarutil independent from Reductionops.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving Refine to its proper module.Gravatar Pierre-Marie Pédrot2016-03-20
* | Making Proofview independent of Logic.Gravatar Pierre-Marie Pédrot2016-03-20
* | Fixing the classification of Tactic Notation.Gravatar Pierre-Marie Pédrot2016-03-20
| * Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving Tacintern to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving the tactic related code from Metasyntax to a new file.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving Print Ltac to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving Tacinterp to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 16:30:33 +0000