diff options
Diffstat (limited to 'tactics/extraargs.ml4')
| -rw-r--r-- | tactics/extraargs.ml4 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 98868e8f9..8215e785a 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -10,6 +10,10 @@ open Pp open Genarg +open Stdarg +open Constrarg +open Pcoq.Prim +open Pcoq.Constr open Names open Tacexpr open Taccoerce |