aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
Commit message (Expand)AuthorAge
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Quickly avoid global axioms in Loic new files about ringGravatar letouzey2011-04-03
* syntax for exponentsGravatar pottier2011-03-08
* Revert "syntax for exponents"Gravatar glondu2011-02-25
* syntax for exponentsGravatar pottier2011-02-22
* anneaux commutatifs ou non, reification sans mlGravatar pottier2011-02-22
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Integer division: quot and rem (trunc convention) in addition to div and modGravatar letouzey2010-11-10
* Still some more Cpow in Type rather than Set (cf. r13542)Gravatar letouzey2010-10-21
* Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)Gravatar letouzey2010-10-14
* Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesGravatar glondu2010-09-30
* Remove some occurrences of "open Termops"Gravatar glondu2010-09-28
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
* Reverting partial fix for #2335 committed by mistake in r13435. Sorry.Gravatar herbelin2010-09-19
* Patch solving the bug but leaving open design choicesGravatar herbelin2010-09-19
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* fixed bug #2316 (ring_simplify)Gravatar barras2010-07-16
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Improvements in generalized rewriting:Gravatar msozeau2010-03-05
* bug in field_simplify_eq inGravatar barras2010-02-10
* Euclidean division for NArithGravatar letouzey2010-02-10
* New command Declare Reduction <id> := <conv_expr>.Gravatar letouzey2010-01-28
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Stop unnecessary use of lazy values for constraints, simplifyingGravatar msozeau2009-09-02
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* nouvelle version de la tactique groebner proposee par Loic:Gravatar barras2009-04-16
* Move setoid_rewrite to its own module and do some clean up inGravatar msozeau2009-04-07
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 05:28:17 +0000