From e3a3b4bb17c40b6af2ef8501c405f0600cc6d65b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 22 Apr 2017 21:09:05 +0200 Subject: Typo in a comment of plugin Quote. --- plugins/quote/quote.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/quote') diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index fc9d70ae7..c649cfb2c 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -8,7 +8,7 @@ (* The `Quote' tactic *) -(* The basic idea is to automatize the inversion of interpetation functions +(* The basic idea is to automatize the inversion of interpretation functions in 2-level approach Examples are given in \texttt{theories/DEMOS/DemoQuote.v} -- cgit v1.2.3