aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/ZMicromega.v
diff options
context:
space:
mode:
authorGravatar fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-05-20 17:01:54 +0000
committerGravatar fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-05-20 17:01:54 +0000
commit7da3e3d85c88eb42e932230048cb0db255474b5d (patch)
tree0cd987e72b528d88c5a2a6bbcfa1d0718a74efa6 /plugins/micromega/ZMicromega.v
parent4c6c284ddc6db47f070026ad68b5c29f6737c4a0 (diff)
added support to handle division by a constant over R
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14147 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/micromega/ZMicromega.v')
-rw-r--r--plugins/micromega/ZMicromega.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 6dad2ba60..f840e471b 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -8,7 +8,7 @@
(* *)
(* Micromega: A reflexive tactic using the Positivstellensatz *)
(* *)
-(* Frédéric Besson (Irisa/Inria) 2006-2008 *)
+(* Frédéric Besson (Irisa/Inria) 2006-2011 *)
(* *)
(************************************************************************)