aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Normalizing the names of dynamic types to follow a typ_* scheme.Pierre-Marie Pédrot
2016-05-04Removing external uses of Val.inject and making Geninterp.interp return Val.tPierre-Marie Pédrot
2016-05-04Removing the Value.of_* API for parameterized types.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Getting rid of the Geninterp.generic_interp function.Pierre-Marie Pédrot
2016-05-04Switching to an untyped toplevel representation for Ltac values.Pierre-Marie Pédrot
2016-05-04Moving Ftactic and Geninterp to the engine folder.Pierre-Marie Pédrot
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03In Regular Subst Tactic mode, ensure that the order of hypotheses isHugo Herbelin
2016-05-03Fix bug #4707: clearbody much slower in 8.5pl1.Pierre-Marie Pédrot
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 06:14:49 +0000