diff options
Diffstat (limited to 'tactics/extraargs.ml4')
| -rw-r--r-- | tactics/extraargs.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index e31428f7c..6bdbdb80b 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -52,7 +52,7 @@ END let pr_int_list = pr_int_list_full () () () -open Rawterm +open Glob_term let pr_occurrences _prc _prlc _prt l = match l with |