diff options
Diffstat (limited to 'contrib/recdef')
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index f973548457..36ebaff11f 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -34,6 +34,7 @@ open Pfedit open Topconstr open Rawterm open Pretyping +open Pretyping.Default open Safe_typing open Constrintern open Hiddentac |