commit by user andrea

[helm.git] / weblib / While / syntax.ma

diff --git a/weblib/While/syntax.ma b/weblib/While/syntax.ma
index 95c93c7e4984816df4948c930c68aa84152dc5e6..8b77cab881aa6fda202fb8b06139967b1657c0e0 100644 (file)
--- 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 *)