diff options
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 27f2292e33..41d92b2331 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -470,7 +470,7 @@ Just testing ... #use "include.ml";; open Quote;; -let r = raw_constr_of_string;; +let r = glob_constr_of_string;; let ivs = { normal_lhs_rhs = |