From 2e3ee15b03cf4b7428e1a7453385d79f434ec4a7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 8 Nov 2015 09:54:42 +0100
Subject: Moving three related small half-general half-ad-hoc utility functions
 next to each other, waiting for possible integration into a more uniform API.

---
 plugins/funind/functional_principles_proofs.ml | 1 +
 plugins/funind/invfun.ml                       | 1 +
 plugins/funind/recdef.ml                       | 1 +
 3 files changed, 3 insertions(+)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c9dd18a2fc..5b9f82aa53 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -9,6 +9,7 @@ open Names
 open Declarations
 open Pp
 open Tacmach
+open Termops
 open Proof_type
 open Tacticals
 open Tactics
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d074bbabd8..363dd1b3b7 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -19,6 +19,7 @@ open Tactics
 open Indfun_common
 open Tacmach
 open Misctypes
+open Termops
 
 (* Some pretty printing function for debugging purpose *)
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index dd5381c760..6867939c26 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -29,6 +29,7 @@ open Proof_type
 open Pfedit
 open Glob_term
 open Pretyping
+open Termops
 open Constrintern
 open Misctypes
 open Genredexpr
-- 
cgit v1.2.3