diff options
Diffstat (limited to 'ltac/taccoerce.ml')
| -rw-r--r-- | ltac/taccoerce.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml index b0a80ef73..df38a42cb 100644 --- a/ltac/taccoerce.ml +++ b/ltac/taccoerce.ml @@ -13,7 +13,6 @@ open Pattern open Misctypes open Genarg open Stdarg -open Constrarg open Geninterp exception CannotCoerceTo of string |