diff options
Diffstat (limited to 'plugins/funind/indfun.mli')
| -rw-r--r-- | plugins/funind/indfun.mli | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index e65b5808..e7206914 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,11 +1,4 @@ -open Util -open Names -open Term -open Pp -open Indfun_common -open Libnames -open Glob_term -open Declarations +open Misctypes val do_generate_principle : bool -> @@ -16,9 +9,9 @@ val do_generate_principle : val functional_induction : bool -> Term.constr -> - (Term.constr * Term.constr Glob_term.bindings) option -> - Genarg.intro_pattern_expr Util.located option -> + (Term.constr * Term.constr bindings) option -> + Tacexpr.or_and_intro_pattern option -> Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma -val make_graph : Libnames.global_reference -> unit +val make_graph : Globnames.global_reference -> unit |