diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c4e0ac500c..ee3e11f8a5 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -24,7 +24,6 @@ open Constrexpr open Constrexpr_ops open Notation_term open Notation_ops -open Topconstr open Nametab open Notation open Inductiveops |