diff options
| author | glondu | 2010-12-24 23:49:17 +0000 |
|---|---|---|
| committer | glondu | 2010-12-24 23:49:17 +0000 |
| commit | 6ebd4c4ad28d46965623e72d8654c36fcc6fe9b0 (patch) | |
| tree | 96640a563162304797535b73f65a5fe8b4811b02 /plugins/funind/rawterm_to_relation.mli | |
| parent | e5b94c29ff49f8b880290a72519157d26351bc6c (diff) | |
Rename files in funind to respect new conventions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13755 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/rawterm_to_relation.mli')
| -rw-r--r-- | plugins/funind/rawterm_to_relation.mli | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/plugins/funind/rawterm_to_relation.mli b/plugins/funind/rawterm_to_relation.mli deleted file mode 100644 index 5c91292bad..0000000000 --- a/plugins/funind/rawterm_to_relation.mli +++ /dev/null @@ -1,16 +0,0 @@ - - - -(* - [build_inductive parametrize funnames funargs returned_types bodies] - constructs and saves the graphs of the functions [funnames] taking [funargs] as arguments - and returning [returned_types] using bodies [bodies] -*) - -val build_inductive : - Names.identifier list -> (* The list of function name *) - (Names.name*Glob_term.glob_constr*bool) list list -> (* The list of function args *) - Topconstr.constr_expr list -> (* The list of function returned type *) - Glob_term.glob_constr list -> (* the list of body *) - unit - |