diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 1 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 7 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
4 files changed, 0 insertions, 11 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 56b1a3f1cb..d6f21fb86b 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -6,7 +6,6 @@ open Vars open Context open Namegen open Names -open Declarations open Declareops open Pp open Entries diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index cc9ae912dc..2dd78d8908 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -18,7 +18,6 @@ open Indfun open Genarg open Tacticals open Misctypes -open Miscops let pr_binding prc = function | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 56fc9bd2cd..91a5ddf826 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,10 +1,3 @@ -open Names -open Term -open Pp -open Indfun_common -open Libnames -open Glob_term -open Declarations open Misctypes val do_generate_principle : diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f951debfde..ca0a432d6a 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -10,7 +10,6 @@ open Term open Vars open Namegen open Environ -open Declarations open Declareops open Entries open Pp @@ -24,7 +23,6 @@ open Tacticals open Tacmach open Tactics open Nametab -open Decls open Declare open Decl_kinds open Tacred |