grafite parser updated

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

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