diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 1 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 6603a95a84..368b23be30 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open Compat open Util open Term diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index c8b4e48337..70333b063d 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open Tacexpr open Declarations open CErrors |