diff options
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 |