aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Remove duplicate definition.Gravatar Guillaume Melquiond2016-01-02
* Remove duplicate declarations.Gravatar Guillaume Melquiond2016-01-02
* Reduce dependencies of interface files.Gravatar Guillaume Melquiond2016-01-02
* Remove useless rec flags.Gravatar Guillaume Melquiond2016-01-02
* Separation of concern in TacAlias API.Gravatar Pierre-Marie Pédrot2016-01-02
* Moving apply_type to new proof engine.Gravatar Hugo Herbelin2015-12-30
* Taking into account generated typing constraints in tactic "generalize".Gravatar Hugo Herbelin2015-12-30
* External tactics and notations now accept any tactic argument.Gravatar Pierre-Marie Pédrot2015-12-30
* Implementing non-focussed generic arguments.Gravatar Pierre-Marie Pédrot2015-12-28
* Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
* Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.Gravatar Pierre-Marie Pédrot2015-12-28
* Factorizing code for untyped constr evaluation.Gravatar Pierre-Marie Pédrot2015-12-27
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-12-27
* Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-12-27
* Moving basic generalization tactics upwards for possible use in "intros".Gravatar Hugo Herbelin2015-12-25
* Moving code of specialize so that it can accept "as" (no semantic change).Gravatar Hugo Herbelin2015-12-25
* Moving specialize to Proofview.tactic.Gravatar Hugo Herbelin2015-12-25
* Fixing a bug in the order of side conditions for introduction pattern -> and <-.Gravatar Hugo Herbelin2015-12-25
* Fixing an "injection as" bug in the presence of side conditions.Gravatar Hugo Herbelin2015-12-25
* Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.mlGravatar Hugo Herbelin2015-12-25
* Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
* Removing the last quoted auto tactic in Tauto.Gravatar Pierre-Marie Pédrot2015-12-24
* Finer-grained types for toplevel values.Gravatar Pierre-Marie Pédrot2015-12-21
* Removing ad-hoc interpretation rules for tactic notations and their genarg.Gravatar Pierre-Marie Pédrot2015-12-21
* Changing the toplevel type of the int_or_var generic type to int.Gravatar Pierre-Marie Pédrot2015-12-21
* Removing the now useless genarg generic argument.Gravatar Pierre-Marie Pédrot2015-12-21
* Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
* Tying the loop in tactic printing API.Gravatar Pierre-Marie Pédrot2015-12-18
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\
* | Getting rid of some hardwired generic arguments.Gravatar Pierre-Marie Pédrot2015-12-17
| * FIx parsing of tactic "simple refine".Gravatar Maxime Dénès2015-12-16
| * Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Gravatar Guillaume Melquiond2015-12-16
| * Refine tactic now shelves unifiable holes.Gravatar Pierre-Marie Pédrot2015-12-15
| * Changing the order of the goals generated by unshelve.Gravatar Pierre-Marie Pédrot2015-12-15
* | Granting clear_flag in injection, even legacy mode. This is possibleGravatar Hugo Herbelin2015-12-15
* | More code sharing between tactic notation and genarg interpretation.Gravatar Pierre-Marie Pédrot2015-12-13
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\|
| * Add tactic native_cast_no_check, analog to vm_cast_no_check.Gravatar Maxime Dénès2015-12-11
| * Fixing a pat%constr bug. Thanks to Enrico for reporting.Gravatar Hugo Herbelin2015-12-10
| * Silently ignore requests to _not_ clear something when that something cannot ...Gravatar Guillaume Melquiond2015-12-10
| * Fixing parsing of the unshelve tactical.Gravatar Pierre-Marie Pédrot2015-12-09
| * Adding an unshelve tactical.Gravatar Pierre-Marie Pédrot2015-12-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* | Fixing compilation with old CAMLPX versions.Gravatar Pierre-Marie Pédrot2015-12-05
* | Removing redundant versions of generalize.Gravatar Hugo Herbelin2015-12-05
* | Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
* | Experimenting removing strong normalization of the mid-statement in tactic cut.Gravatar Hugo Herbelin2015-12-05
* | Moving three related small half-general half-ad-hoc utility functionsGravatar Hugo Herbelin2015-12-05
* | Getting rid of some quoted tactics in Tauto.Gravatar Pierre-Marie Pédrot2015-12-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 20:20:36 +0000