X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2FWhile%2Fsyntax.ma;fp=weblib%2FWhile%2Fsyntax.ma;h=8b77cab881aa6fda202fb8b06139967b1657c0e0;hb=bcbd3124423b5e95855da2a34a126b59caa9a3f8;hp=95c93c7e4984816df4948c930c68aa84152dc5e6;hpb=ef335c7310bd175a2df936eb284fed6142ee0b6e;p=helm.git

diff --git a/weblib/While/syntax.ma b/weblib/While/syntax.ma
index 95c93c7e4..8b77cab88 100644
--- a/weblib/While/syntax.ma
+++ b/weblib/While/syntax.ma
@@ -23,7 +23,7 @@ inductive Aexp : Type[0] ≝
  .
 
 interpretation "Aexp plus" 'plus x y = (Add x y).
-interpretation "Aexp minus" 'plus x y = (Sub x y).
+interpretation "Aexp minus" 'minus x y = (Sub x y).
 interpretation "Aexp times" 'times x y = (Mul x y).
 
 (* Boolean expressions *)