aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYves Bertot2018-05-11 17:24:18 +0200
committerYves Bertot2018-05-11 17:24:18 +0200
commitd558653e3a0ecc0b182f5e84a8db474d7a5aa1f8 (patch)
tree09608d823d5848bc336f4c49a7c104b7a83d6ff9
parent1117a348c1ca11833ae12361500d08c62fd8f76b (diff)
Updates the contents of the third tutorial
-rw-r--r--README.md3
1 files changed, 1 insertions, 2 deletions
diff --git a/README.md b/README.md
index 00ff146e46..417a511f82 100644
--- a/README.md
+++ b/README.md
@@ -42,9 +42,8 @@ How to write plugins in Coq
- Obtaining existing values from memory
- Composing values
- Verifying types
- - Leveraging type inference
- - Leveraging coercion
- Using these terms in commands
- Using these terms in tactics
+ - Automatic proofs without tactics using type classes and canonical structures
compilation and loading must be performed as for `tuto0`.