diff options
Diffstat (limited to 'tactics/taccoerce.mli')
| -rw-r--r-- | tactics/taccoerce.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli index 75a3b347d..82e1910f7 100644 --- a/tactics/taccoerce.mli +++ b/tactics/taccoerce.mli @@ -12,6 +12,7 @@ open Term open Misctypes open Pattern open Genarg +open Geninterp (** Coercions from highest level generic arguments to actual data used by Ltac interpretation. Those functions examinate dynamic types and try to return |