aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
AgeCommit message (Expand)Author
2017-03-14Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunMaxime Dénès
2017-02-17Moving the Ltac plugin to a pack-based one.Pierre-Marie Pédrot
2017-02-16[cleanup] Change Id.t option to Name.t in TacFunTej Chajed
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers related to printing.Pierre-Marie Pédrot
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Removing some return type compatibility layers in Termops.Pierre-Marie Pédrot
2017-02-14Setoid_ring API using EConstr.Pierre-Marie Pédrot
2017-02-14Quote API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Rewrite API using EConstr.Pierre-Marie Pédrot
2017-02-14Goal API using EConstr.Pierre-Marie Pédrot
2017-02-14Typing API using EConstr.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-29Ncring_initial: avoid a notation overridingPierre Letouzey
2016-09-28Ring_theory: avoid overriding a few notationsPierre Letouzey
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-09-15Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Pierre-Marie Pédrot
2016-09-14Moving Ltac-specific parsing API to ltac/ folder.Pierre-Marie Pédrot
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-24Removing tactic compatibility layers in setoid_ring.Pierre-Marie Pédrot
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-16Adding printers for ring and field commands.Hugo Herbelin
2016-06-16Remove inappropriate comment.Maxime Dénès
2016-06-14Merge remote-tracking branch 'github/evarunsafe' into trunkMatthieu Sozeau
2016-06-09newring: fix for hack using evars as integers.Matthieu Sozeau
2016-06-08Compilation via pack for plugins of the stdlibPierre Letouzey
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-04-27Revert "Adding printers for ring and field commands."Hugo Herbelin
2016-04-27Adding printers for ring and field commands.Hugo Herbelin
2016-04-01Getting rid of the "_mods" parsing entry.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic entries defined by Coq itself.Pierre-Marie Pédrot
2016-03-06Removing useless grammar.cma dependencies.Pierre-Marie Pédrot
2016-03-04Making parentheses mandatory in tactic scopes.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-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-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-30External tactics and notations now accept any tactic argument.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 15:13:13 +0000