diff options
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index cb41de283..e2dc149b0 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -7,11 +7,6 @@ open Names open Declarations open Pp open Entries -open Hiddentac -open Evd -open Tacmach -open Proof_type -open Tacticals open Tactics open Indfun_common open Functional_principles_proofs |