aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Fixing #4787 (Unset Bracketing Last Introduction Pattern not working).Gravatar Hugo Herbelin2016-06-07
* Removing the Q_constr file.Gravatar Pierre-Marie Pédrot2016-06-05
* Moving Hipattern to a regular ML file.Gravatar Pierre-Marie Pédrot2016-06-05
* Removing PATTERN uses in Hipattern.Gravatar Pierre-Marie Pédrot2016-06-05
* Add a synonymous Set Debug Typeclasses for Set Typeclasses Debug, for uniform...Gravatar Hugo Herbelin2016-06-02
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\
| * Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| * Fix bug #4746: Anomaly: Evar ?X10 was not declared.Gravatar Pierre-Marie Pédrot2016-05-29
| * rewrite/Univs: Fix bug # 4498.Gravatar Matthieu Sozeau2016-05-26
| * Hints/Univs: fix bug #4628 anomaliesGravatar Matthieu Sozeau2016-05-23
* | 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
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 00:15:05 +0000