diff options
Diffstat (limited to 'contrib/extraction/test_extraction.v')
| -rw-r--r-- | contrib/extraction/test_extraction.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v index ad95428f1f..70ca40c4ff 100644 --- a/contrib/extraction/test_extraction.v +++ b/contrib/extraction/test_extraction.v @@ -435,4 +435,13 @@ Extraction loop. let rec f a = f (S a) in f O -*)
\ No newline at end of file +*) + +Extraction "test" + nat test1 c test2 test3 test4 test5 test6 test7 + d d2 d3 d4 d5 d6 test8 id' id'' test9 Finite test10 test11 + test12 tree tree_size test13 sumbool_rect predicate test14 + test15 eta_c test16 test17 test18 bidon tb fbidon fbidon2 + fbidon2 test_0 test_1 eq eq_rect test19 tp1 tp1bis test20 + horibilis PropSet natbool zerotrue zeroTrue zeroprop test21 test22 + test23 f f_prop f_arity f_normal Truc oups test24 loop. |