diff options
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 1d275c1aa..d6f847cc7 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -65,6 +65,7 @@ let get_new_id locals id = (** Inductive declarations *) +open Context open Termops open Reduction |