X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2FWhile%2Fsyntax.ma;h=8b77cab881aa6fda202fb8b06139967b1657c0e0;hb=cd2f5b59215ea771ac137b9a7b115a05175f45d5;hp=95c93c7e4984816df4948c930c68aa84152dc5e6;hpb=e0671ce496760cec78ec904747af76ed55fd03a2;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 *)