aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/Micromega.tex
AgeCommit message (Collapse)Author
2018-03-22[Sphinx] Move chapter 22 to new infrastructureMaxime Dénès
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2016-08-30plugin micromega : nra also handles non-linear rational arithmetic over Q ↵Frédéric Besson
(Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R.
2015-07-31Fix typos in the Micromega part of the reference manual.Guillaume Melquiond
2015-07-30Fix some broken Coq scripts in the documentation.Guillaume Melquiond
2014-12-09refman: switch all source files to utf8Pierre Letouzey
Putting utf8 everywhere helps the maintainance of the online refman. And anyway, this is the way to go. We should also chase and migrate the few remaining iso-latin-1 files elsewhere in the sources.
2014-09-11Fixing bug #3605.Pierre-Marie Pédrot
2014-08-25Grammar: "allowing to" is not proper EnglishJason Gross
I'm not quite sure why, but I'm pretty sure it's not. Rather, in "allowing for foo" and "allowing to foo", "foo" modifies the sense in which someting is allowed, rather than it being "foo" that's allowed. "Allowing fooing" generally works, though it can sound a bit awkward. "Allowing one to foo" (or "Allowing {him,her,it,Coq} to foo") is always acceptable, in-as-much as it's ok to use "one". I haven't touched the older instances of it in the CHANGES file.
2013-12-20micromega: removal of spurious Export; addition of Lia.v encapsulating lia ↵Frédéric Besson
and nia.
2011-06-29update of Micromega docfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14248 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-24Micromega doc : psatz Z -> psatz Z 2fbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12353 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-25git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 ↵fbesson
85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-13update doc Micromegafbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11223 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-07Micromega: doc + test-suite updatefbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11211 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-02Improved robustness of micromega parser. Proof search of Micromega ↵fbesson
test-suites is now bounded -- ensure termination git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11200 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-25Micromega : bugs fixes - renaming of tactics - documentationfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11173 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 07:58:28 +0000