aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
2016-04-15Merge remote-tracking branch 'OFFICIAL/trunk' into morefreshPierre Courtieu
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-07Allow to unset the refinement mode of Instance in MLMatthieu Sozeau
2016-04-07Fixing an incorrect use of prod_appvect on a term which was not aHugo Herbelin
2016-04-03Fixing the "No applicable tactic" non informative error messageHugo Herbelin
2016-03-25Moving Autorewrite back to tactics/.Pierre-Marie Pédrot
2016-03-25Moving Eqdecide to tactics/.Pierre-Marie Pédrot
2016-03-25Moving Eauto and Class_tactics to tactics/.Pierre-Marie Pédrot
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2016-03-20Moving Tacsubst to hightactics.Pierre-Marie Pédrot
2016-03-20Relying on generic arguments to represent Extern hints.Pierre-Marie Pédrot
2016-03-20Adding a new Ltac generic argument for forced tactics returing unit.Pierre-Marie Pédrot
2016-03-20Moving Tacenv to Hightactics.Pierre-Marie Pédrot
2016-03-20Moving Tactic_debug to Hightactic.Pierre-Marie Pédrot
2016-03-20Making Evarutil independent from Reductionops.Pierre-Marie Pédrot
2016-03-20Moving Refine to its proper module.Pierre-Marie Pédrot
2016-03-20Making Proofview independent of Logic.Pierre-Marie Pédrot
2016-03-20Fixing the classification of Tactic Notation.Pierre-Marie Pédrot
2016-03-20Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.Pierre-Marie Pédrot
2016-03-20Moving Tacintern to Hightactics.Pierre-Marie Pédrot
2016-03-20Moving the Ltac definition command to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving the tactic related code from Metasyntax to a new file.Pierre-Marie Pédrot
2016-03-20Moving Print Ltac to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Tactic Notation to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Tacinterp to Hightactics.Pierre-Marie Pédrot
2016-03-19Moving the use of Tactic_option from Obligations to G_obligations.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic arguments defined by Coq itself.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic entries defined by Coq itself.Pierre-Marie Pédrot
2016-03-17Adding a universe argument to Pcoq.create_generic_entry.Pierre-Marie Pédrot
2016-03-17Removing the registering of default values for generic arguments.Pierre-Marie Pédrot
2016-03-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-09Redo fix init_setoid -> init_relation_classesMatthieu Sozeau
2016-03-09Fix strategy of Keyed UnificationMatthieu Sozeau
2016-03-06Moving Autorewrite to Hightatctic.Pierre-Marie Pédrot
2016-03-06Putting Tactic_debug just below Tacinterp.Pierre-Marie Pédrot
2016-03-06Removing dependency of Himsg in tactic files.Pierre-Marie Pédrot
2016-03-06Moving Tactic_debug to tactics/ folder.Pierre-Marie Pédrot
2016-03-06Moving Ltac traces to Tacexpr and Tacinterp.Pierre-Marie Pédrot
2016-03-06Removing useless grammar.cma dependencies.Pierre-Marie Pédrot
2016-03-06Moving Eauto to a simple ML file.Pierre-Marie Pédrot
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-05Exporting build_selector, a component of discriminate, for use in congruence.Hugo Herbelin
2016-03-04Adding some standard arguments in tactic scopes.Pierre-Marie Pédrot
2016-03-04Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].Pierre-Marie Pédrot
2016-03-04Removing the UConstr entry of the tactic_arg AST.Pierre-Marie Pédrot
2016-02-29Moving the "move" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "exists" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "symmetry" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "generalize dependent" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 16:37:02 +0000