diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-22 21:09:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-13 12:19:23 +0200 |
| commit | e3a3b4bb17c40b6af2ef8501c405f0600cc6d65b (patch) | |
| tree | d038fd28fc8ea222557ce492998a27a723371e04 /plugins/quote | |
| parent | ba88e99d37817cd3a591b14bbceb61e28f3e3382 (diff) | |
Typo in a comment of plugin Quote.
Diffstat (limited to 'plugins/quote')
| -rw-r--r-- | plugins/quote/quote.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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} |