aboutsummaryrefslogtreecommitdiff
path: root/plugins/ring/ring.ml
AgeCommit message (Expand)Author
2020-11-16Improve some error messages.Vincent Semeria
2020-11-16Other renamings evd -> sigma in newring.ml.Hugo Herbelin
2020-11-16Pass sigma functionally in newring.ml.Hugo Herbelin
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
2012-07-05Legacy Ring and Legacy Field migrated to contribsletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-02Noise for nothingpboutill
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-07-29Ring: replaced various generic = on constr by eq_constr, destructors etc.puech
2011-07-29Ring: replaced some generic Pervasives.compare on constr by constr_ordpuech
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2009-12-12Updated compatibility for rewriting equality proofs that are dependentherbelin
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-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-08-03Added "etransitivity".herbelin
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey