aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/functional_principles_types.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/functional_principles_types.mli')
-rw-r--r--plugins/funind/functional_principles_types.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 2eb1b7935..a3315f22c 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
val generate_functional_principle :
Evd.evar_map ref ->