aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2015-12-25Fixing an "injection as" bug in the presence of side conditions.Hugo Herbelin
2015-12-25Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.mlHugo Herbelin
2015-12-24Removing auto from the tactic AST.Pierre-Marie Pédrot
2015-12-24Removing the last quoted auto tactic in Tauto.Pierre-Marie Pédrot
2015-12-21Finer-grained types for toplevel values.Pierre-Marie Pédrot
2015-12-21Removing ad-hoc interpretation rules for tactic notations and their genarg.Pierre-Marie Pédrot
2015-12-21Changing the toplevel type of the int_or_var generic type to int.Pierre-Marie Pédrot
2015-12-21Removing the now useless genarg generic argument.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-12-18Tying the loop in tactic printing API.Pierre-Marie Pédrot
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-17Getting rid of some hardwired generic arguments.Pierre-Marie Pédrot
2015-12-16FIx parsing of tactic "simple refine".Maxime Dénès
2015-12-16Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Guillaume Melquiond
2015-12-15Refine tactic now shelves unifiable holes.Pierre-Marie Pédrot
2015-12-15Changing the order of the goals generated by unshelve.Pierre-Marie Pédrot
2015-12-15Granting clear_flag in injection, even legacy mode. This is possibleHugo Herbelin
2015-12-13More code sharing between tactic notation and genarg interpretation.Pierre-Marie Pédrot
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-11Add tactic native_cast_no_check, analog to vm_cast_no_check.Maxime Dénès
2015-12-10Fixing a pat%constr bug. Thanks to Enrico for reporting.Hugo Herbelin
2015-12-10Silently ignore requests to _not_ clear something when that something cannot ...Guillaume Melquiond
2015-12-09Fixing parsing of the unshelve tactical.Pierre-Marie Pédrot
2015-12-09Adding an unshelve tactical.Pierre-Marie Pédrot
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-05Fixing compilation with old CAMLPX versions.Pierre-Marie Pédrot
2015-12-05Removing redundant versions of generalize.Hugo Herbelin
2015-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
2015-12-05Experimenting removing strong normalization of the mid-statement in tactic cut.Hugo Herbelin
2015-12-05Moving three related small half-general half-ad-hoc utility functionsHugo Herbelin
2015-12-05Getting rid of some quoted tactics in Tauto.Pierre-Marie Pédrot
2015-12-04Getting rid of the dynamic node of the tactic AST.Pierre-Marie Pédrot
2015-12-04Fix in setoid_rewrite in Type: avoid the generation of a rigid universeMatthieu Sozeau
2015-12-04Removing the last use of valueIn in Tauto.Pierre-Marie Pédrot
2015-12-04Removing dynamic inclusion of constrs in tactic AST.Pierre-Marie Pédrot
2015-12-03Removing the globTacticIn primitive.Pierre-Marie Pédrot
2015-12-03Fixing Tauto compilation for older versions of OCaml.Pierre-Marie Pédrot
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-03Removing the last use of tacticIn in setoid_ring.Pierre-Marie Pédrot
2015-12-03Removing the use of tacticIn in Tauto.Pierre-Marie Pédrot
2015-12-02Slight simplification of code for pat/constr.Hugo Herbelin
2015-12-02Dead code from August 2014 in apply in.Hugo Herbelin
2015-12-02Removing dead code in Obligations.Pierre-Marie Pédrot
2015-11-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-27Fix [Polymorphic Hint Rewrite].Matthieu Sozeau
2015-11-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-23Fix generation of equality schemes on polymorphic equality types.Matthieu Sozeau
2015-11-23Removing a use of old refine in Tactics.Pierre-Marie Pédrot
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 20:28:00 +0000