aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-01-12 12:56:07 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-01-12 12:56:07 +0100
commit4b8cd99705596052b7b45f29c248c9d02875ccdc (patch)
tree45d4145f03723025eb75781525fedd478d32e5a1 /test-suite/output
parentbd3acff29dbdbf329d9ef6a92289e504ef688803 (diff)
Fixing name of evars in output test Notation.v.
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Notations.out7
1 files changed, 4 insertions, 3 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 7856bb6f6..60ee72b36 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -111,13 +111,14 @@ fun x : option Z => match x with
| NONE2 => 0
end
: option Z -> Z
-fun x : list ?T0 => match x with
+fun x : list ?T1 => match x with
| NIL => NONE2
| (_ :') t => SOME2 t
end
- : list ?T0 -> option (list ?T0)
+ : list ?T1 -> option (list ?T1)
where
-?T0 : [x : list ?T0 |- Type] (x cannot be used)
+?T1 : [x : list ?T1 x1 : list ?T1 x0 := x1 : list ?T1 |- Type] (x, x1,
+ x0 cannot be used)
s
: s
10