aboutsummaryrefslogtreecommitdiff
path: root/plugins/ring
AgeCommit message (Expand)Author
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
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-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
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-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
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
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
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-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-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...letouzey
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-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey