From bcbd3124423b5e95855da2a34a126b59caa9a3f8 Mon Sep 17 00:00:00 2001
From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Wed, 10 Apr 2013 11:44:22 +0000
Subject: [PATCH] commit by user andrea

---
 weblib/While/syntax.ma | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 *)
-- 
2.39.2