testsuite: fix test of generate_trees

There were two differences between the current output and the old gold file: 

  1. The trees are no longer generated with increasing depth
  2. The meaning of the -depth flag has changed: for example, 
     "gt -cat=Nat -depth=1" used to generate only "zero",
     now you also get "succ zero".
This commit is contained in:
hallgren
2013-12-10 16:49:40 +00:00
parent e4246d090c
commit 4e1df7eb59
2 changed files with 15 additions and 14 deletions

View File

@@ -1,5 +1,5 @@
-- here we test that the abstract operations are not used for proof search
i testsuite/compiler/check/abstract-operations/Nat.gf
gt -cat=Nat -number=10 -depth=10
gt -cat=Nat -number=11 -depth=10
pt -compute (twice (succ zero))