X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2FWhile%2Fsyntax.ma;h=8b77cab881aa6fda202fb8b06139967b1657c0e0;hb=bf7be462a06e739b39af20f72362857e849a2aa0;hp=b55d89d438b7f238f013830fed30b36d9765bb4f;hpb=0c94f81f769d3c7377811a584f647553ebe7ceaf;p=helm.git

diff --git a/weblib/While/syntax.ma b/weblib/While/syntax.ma
index b55d89d43..8b77cab88 100644
--- a/weblib/While/syntax.ma
+++ b/weblib/While/syntax.ma
@@ -7,7 +7,7 @@ include "arithmetics/nat.ma".
 
 (* Variables *)
 
-inductive Var : Type[0] ≝
+ inductive Var : Type[0] ≝
   Id : nat → Var.
  
 (* Arithmetic expressions *)
@@ -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 *)