diff options
| author |  Julien Forest <julien.forest@ensiie.fr> | 2014-12-11 21:13:14 +0100 |
|---|---|---|
| committer | Julien Forest <julien.forest@ensiie.fr> | 2014-12-11 21:13:44 +0100 |
| commit | dbe6df0d591bc6ac843360a3998f947d56298d4f (patch) | |
| tree | d81188d103a4b4cc921f8767dbc695ba8a450239 /plugins/funind/glob_term_to_relation.mli | |
| parent | cf90fc69d609c1208036faa1a8b8945f975d2cef (diff) | |
handling Functional Scheme for required but not imported modules
Diffstat (limited to 'plugins/funind/glob_term_to_relation.mli')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index 101be24fd..b0a05ec32 100644 --- a/plugins/funind/glob_term_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli @@ -7,6 +7,7 @@ open Names *) val build_inductive : + (ModPath.t * DirPath.t) option -> Id.t list -> (* The list of function name *) (Name.t*Glob_term.glob_constr*bool) list list -> (* The list of function args *) Constrexpr.constr_expr list -> (* The list of function returned type *) |