diff options
Diffstat (limited to 'intf/tacexpr.mli')
| -rw-r--r-- | intf/tacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index d8e340d1e8..e70fc13086 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Topconstr +open Constrexpr open Libnames open Nametab open Genredexpr |