summaryrefslogtreecommitdiff
path: root/contrib/funind/rawterm_to_relation.mli
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind/rawterm_to_relation.mli')
-rw-r--r--contrib/funind/rawterm_to_relation.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/funind/rawterm_to_relation.mli b/contrib/funind/rawterm_to_relation.mli
index 9cd04123..0075fb0a 100644
--- a/contrib/funind/rawterm_to_relation.mli
+++ b/contrib/funind/rawterm_to_relation.mli
@@ -1,5 +1,6 @@
+
(*
[build_inductive parametrize funnames funargs returned_types bodies]
constructs and saves the graphs of the functions [funnames] taking [funargs] as arguments
@@ -7,7 +8,6 @@
*)
val build_inductive :
- bool -> (* if true try to detect parameter. Always use it as true except for debug *)
Names.identifier list -> (* The list of function name *)
(Names.name*Rawterm.rawconstr*bool) list list -> (* The list of function args *)
Topconstr.constr_expr list -> (* The list of function returned type *)