diff options
| author | Maxime Dénès | 2017-05-17 09:03:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-17 09:03:09 +0200 |
| commit | 5360ec8ff56c44e96c56965be78e6f2538963a57 (patch) | |
| tree | 82361651080323e8ab33db31890c32b93f6928ea /plugins | |
| parent | 5ea95f9cd843bec4504646851bf22bf505e56ad8 (diff) | |
| parent | 9ddfdab6a4715a08a78296bf8824d086f358bdc0 (diff) | |
Merge PR#636: Miscellaneous typos, dead code, etc.
Diffstat (limited to 'plugins')
| -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 fc9d70ae7d..c649cfb2c6 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} |