aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
AgeCommit message (Expand)Author
2016-09-29Ncring_initial: avoid a notation overridingPierre Letouzey
2016-09-28Ring_theory: avoid overriding a few notationsPierre Letouzey
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
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-04Getting rid of dynamic hacks in Setoid_newring.Pierre-Marie Pédrot
2015-12-03Removing the last use of tacticIn in setoid_ring.Pierre-Marie Pédrot
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-20Proofview.Goal.sigma returns an indexed evarmap.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Univs: fix evar_map initialization in newring.Matthieu Sozeau
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-02-12Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Hugo Herbelin
2015-02-12Capital letter in plugins.Hugo Herbelin
2015-01-25Adding a proper interface to Newring.Pierre-Marie Pédrot
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-10-31Feedback message: hold extra info to help routingEnrico Tassi
2014-10-27Removing an Evd.merge in Newring.Pierre-Marie Pédrot
2014-10-27Fix some typos in comments.Guillaume Melquiond
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-10-01Fix cbn behavior wrt simpl no matchPierre Boutillier
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:57:07 +0000