aboutsummaryrefslogtreecommitdiff
path: root/contrib/setoid_ring/Field_theory.v
AgeCommit message (Collapse)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵letouzey
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-17- gros commit sur ring et field: passage des arguments simplifiebarras
- tacinterp.ml: les arguments tactiques de Tactic Notation n'etaient pas evalues, laissant des variables libres (symptome: exc Not_found) - reals: Open Local --> Local Open - ListTactics: syntaxe des listes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11989 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-22A try at allowing matching on applications as a binary syntax node by default.msozeau
It breaks tauto as [?X _ _] matches much more terms. It is mostly fixed by not destructing objects of record types. The new [intuition] was also pulling an unneeded dependency in Field_theory which can be cleared easily. Zis_gcd_bezout is also considered a conjunction now, which seems correct(?). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11243 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-21refined the conversion oraclebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10960 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-07Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partmsozeau
of the fix I added an optional "by" annotation for rewrite to solve said conditions in the same tactic call. Most of the theories have been updated, only FSets is missing, Pierre will take care of it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-18Petite correction suite à la révision 10571notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10575 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-07Replaced BinNat with a new version that is based on ↵emakarov
theories/Numbers/Natural/Binary/NBinDefs. Most of the entities in the new BinNat are notations for the development in Numbers. Also added min and max to the new natural numbers and integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10298 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-29Orthographe en passantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9815 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-05changement dans ring specification du sign, divisionbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9591 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-02Now 1/x * x simplifies to 1thery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9585 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-24changement de la fonction norm_substbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9529 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-15Changement dans ring et field, beaucoup de correction d'erreurs,bgregoir
maintenant les differentes tactics marchent mieux mais le code est moche ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9454 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-11Changement dans le kernel : bgregoir
- essai de suppression des dependances debiles. (echec) - Application des patch debian. Pour ring et field : - introduciton de la function de sign et de puissance. - Correction de certains bug. - supression de ring_replace .... Pour exact_no_check : - ajout de la tactic : vm_cast_no_check (t) qui remplace "exact_no_check (t<: type of Goal)" (cette version forcais l'evaluation du cast dans le pretypage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-27simplif de la partie ML de ring/fieldbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9302 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-27changement des _sym par _comm dans setoid_ringbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9299 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17field_simplify_eq profite de la factorisation de Laurentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9248 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-16changes the use of lists and notations, to avoid that the notationsbertot
from BinList hide the 'List' type as soon as one requires a ring tactic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9242 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-12Fix name clash on leftthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9234 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-10Remove duplicate conditions in Field + Monomial substitution function for PExprthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9230 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-02bug dans field_simplifybarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9196 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-29args implicites dans Fieldbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9192 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-28separation de RealFieldbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9187 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 20:30:07 +0000