diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
| commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
| tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /plugins/funind/indfun.mli | |
| parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) | |
Imported Upstream version 8.5~beta1+dfsg
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 |