diff options
| author | Hugo Herbelin | 2015-11-08 09:54:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-05 08:58:20 +0100 |
| commit | 2e3ee15b03cf4b7428e1a7453385d79f434ec4a7 (patch) | |
| tree | fc399b19682aa528a73d90729c1e37ce4a761d6e /plugins | |
| parent | f22ad605a14eb14d11b0a1615f7014f2dca3b483 (diff) | |
Moving three related small half-general half-ad-hoc utility functions
next to each other, waiting for possible integration into a more
uniform API.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 1 |
3 files changed, 3 insertions, 0 deletions
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 |