aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
AgeCommit message (Expand)Author
2011-05-05Setoid_ring: some cleanups related with BinPos and BinNatletouzey
2011-05-05Modularization of BinPos + fixes in Stdlibletouzey
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-04-03Quickly avoid global axioms in Loic new files about ringletouzey
2011-03-08syntax for exponentspottier
2011-02-25Revert "syntax for exponents"glondu
2011-02-22syntax for exponentspottier
2011-02-22anneaux commutatifs ou non, reification sans mlpottier
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-11-10Integer division: quot and rem (trunc convention) in addition to div and modletouzey
2010-10-21Still some more Cpow in Type rather than Set (cf. r13542)letouzey
2010-10-14Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)letouzey
2010-09-30Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesglondu
2010-09-28Remove some occurrences of "open Termops"glondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
2010-09-19Reverting partial fix for #2335 committed by mistake in r13435. Sorry.herbelin
2010-09-19Patch solving the bug but leaving open design choicesherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
2010-07-16fixed bug #2316 (ring_simplify)barras
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-03-05Improvements in generalized rewriting:msozeau
2010-02-10bug in field_simplify_eq inbarras
2010-02-10Euclidean division for NArithletouzey
2010-01-28New command Declare Reduction <id> := <conv_expr>.letouzey
2009-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...letouzey
2009-11-03OrderedType implementation for various numerical datatypes + min/max structuresletouzey
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Remove useless Liboject.export_function fieldglondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-09-02Stop unnecessary use of lazy values for constraints, simplifyingmsozeau
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-04-16nouvelle version de la tactique groebner proposee par Loic:barras
2009-04-07Move setoid_rewrite to its own module and do some clean up inmsozeau
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 20:09:00 +0000