aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Merge PR #100: fresh now accepts more things than just identifiers.Gravatar Pierre-Marie Pédrot2016-06-16
|\
* \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-13
|\ \
| * | Fixing a try with in apply that has become too weak in 8.5.Gravatar Hugo Herbelin2016-06-11
* | | Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
| * | Improve the interpretation scope of arguments of an ltac match.Gravatar Hugo Herbelin2016-06-09
* | | 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 remote-tracking branch 'OFFICIAL/trunk' into morefreshGravatar Pierre Courtieu2016-04-15
| | |\ | |_|/ |/| |
* | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 10:14:29 +0000