aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring/Field_theory.v
AgeCommit message (Expand)Author
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-05-06Fix extraction taking a type in the wrong environment.Matthieu Sozeau
2014-05-06Try a new way of handling template universe levelsMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-11-21Field_theory: nicer notations for constants 0 1 ...Pierre Letouzey
2013-08-23Fixing an incompleteness of the ring/field tacticsamahboub
2013-08-22Correcting misplaced Proof command.amahboub
2013-08-22Fixing a significant efficiency leak in the code of the field tactic.amahboub
2013-08-22Field_theory : faster and nicer proofs + nice notations.letouzey
2013-01-18Unset Asymmetric Patternspboutill
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-08-08Updating headers.herbelin
2012-07-19Getting rid of the undocumented [complete] tactic, which wasppedrot
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2011-06-21Follow-up concerning eqb / ltb / leb comparisonsletouzey
2011-05-05BinInt: Z.add become the alternative Z.add'letouzey
2011-05-05Modularization of BinInt, related fixes in the stdlibletouzey
2011-05-05Setoid_ring: some cleanups related with BinPos and BinNatletouzey
2011-05-05Modularization of BinPos + fixes in Stdlibletouzey
2010-10-21Still some more Cpow in Type rather than Set (cf. r13542)letouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2009-11-03OrderedType implementation for various numerical datatypes + min/max structuresletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
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-16 05:57:10 +0000