aboutsummaryrefslogtreecommitdiff
path: root/contrib/micromega/Refl.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
2008-05-19Intégration de micromega ("omicron" pour fourier et sa variante sur Z,herbelin
"micromega" et "sos" pour les problèmes non linéaires sous-traités à csdp); mise en place d'un cache pour pouvoir rejouer les preuves sans avoir besoin de csdp (pour l'instant c'est du bricolage, faudra affiner cela). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10947 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-16Added transitivity and irreflexivity of <, as well as < -elimination for ↵emakarov
binary positive numbers. Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10226 85f007b7-540e-0410-9357-904b9bb8a0f7