aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2016-02-29Moving the "clearbody" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clear" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "cofix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "fix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-28Fixing bug #4596: [rewrite] broke in the past few weeks.Pierre-Marie Pédrot
2016-02-27Removing Tacmach.New qualification in Tacinterp.Pierre-Marie Pédrot
2016-02-27Removing some compatibility layers in Tacinterp.Pierre-Marie Pédrot
2016-02-24Removing the MetaIdArg entry of tactic expressions.Pierre-Marie Pédrot
2016-02-24Getting rid of the "<:tactic< ... >>" quotations.Pierre-Marie Pédrot
2016-02-23Moving tauto.ml4 to a proper ML file.Pierre-Marie Pédrot
2016-02-23Fix bug #4544: Backtrack on using full betaiota reduction during keyed unific...Matthieu Sozeau
2016-02-22Moving the Tauto tactic to proper Ltac.Pierre-Marie Pédrot
2016-02-22The tactic generic argument now returns a value rather than a glob_expr.Pierre-Marie Pédrot
2016-02-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-19Fix regression from 8.4 in reflexivity/...Matthieu Sozeau
2016-02-18FIX: of my previous merging mistakeMatej Kosik
2016-02-17Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").Pierre-Marie Pédrot
2016-02-17CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-02-16Tacticals: typo in a commentPierre Letouzey
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Using monotonic types for conversion functions.Pierre-Marie Pédrot
2016-02-15Code factorization of tactic "unfold_body".Pierre-Marie Pédrot
2016-02-15More conversion functions in the new tactic API.Pierre-Marie Pédrot
2016-02-15Moving conversion functions to the new tactic API.Pierre-Marie Pédrot
2016-02-15Renaming functions in Typing to stick to the standard e_* scheme.Pierre-Marie Pédrot
2016-02-15Monotonizing the Evarutil module.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 04:36:52 +0000