diff options
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 04e0b352c..1c677de95 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -26,7 +26,7 @@ open Reduction open Cases open Logic open Printer -open Rawterm +open Glob_term open Evd let pr_lconstr c = quote (pr_lconstr c) |