diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 4 |
2 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 32120a9674..799d310fa7 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -31,6 +31,8 @@ Let "x" e1 e2 : expr Let "x" e1 e2 : expr +Let "x" e1 e2 : list string + : list string myAnd1 True True : Prop r 2 3 diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index d3433949d1..26c7840a16 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -94,6 +94,10 @@ Coercion App : expr >-> Funclass. Check (Let "x" e1 e2). +Axiom free_vars :> expr -> list string. + +Check (Let "x" e1 e2) : list string. + End D. (* Fixing bugs reported by G. Gonthier in #9207 *) |