aboutsummaryrefslogtreecommitdiff
path: root/coq/ML4PG/libs/ssreflect/jvm/expt_names
diff options
context:
space:
mode:
Diffstat (limited to 'coq/ML4PG/libs/ssreflect/jvm/expt_names')
-rw-r--r--coq/ML4PG/libs/ssreflect/jvm/expt_names6
1 files changed, 6 insertions, 0 deletions
diff --git a/coq/ML4PG/libs/ssreflect/jvm/expt_names b/coq/ML4PG/libs/ssreflect/jvm/expt_names
new file mode 100644
index 00000000..3678e929
--- /dev/null
+++ b/coq/ML4PG/libs/ssreflect/jvm/expt_names
@@ -0,0 +1,6 @@
+1 helper_expt_is_theta
+2 fn_expt_is_theta
+3 loop_is_helper_expt
+4 program_is_fn_expt
+5 program_correct_expt
+6 total_correctness_expt