aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/README2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/README b/plugins/extraction/README
index 64c871fd3..a9a7b04d5 100644
--- a/plugins/extraction/README
+++ b/plugins/extraction/README
@@ -6,7 +6,7 @@
What is it ?
------------
-The extraction is a mechanism allowing to produce functional code
+The extraction is a mechanism that produces functional code
(Ocaml/Haskell/Scheme) out of any Coq terms (either programs or
proofs).