aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/indfun_common.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/indfun_common.mli')
-rw-r--r--plugins/funind/indfun_common.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 1e0b95df34..102994f61e 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -70,6 +70,7 @@ type function_info =
rect_lemma : Constant.t option;
rec_lemma : Constant.t option;
prop_lemma : Constant.t option;
+ sprop_lemma : Constant.t option;
is_general : bool;
}