]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/tests/replace.ma
ocaml 3.09 transition
[helm.git] / helm / matita / tests / replace.ma
index 8504b6c160c78eb5298c5d276fa3cc80b2109933..b5d1eb355514bec21c75b0775e3bfffd01c82b8e 100644 (file)
@@ -35,5 +35,5 @@ qed.
 
 (* This test tests "replace in match t" where t contains some metavariables *)
 theorem t2: 2 + (3 * 4) = (5 + 5) + 2 * 2.
- replace in match 5+? with (6 + 4); [reflexivity | reflexivity].
+ replace in match (5+?) with (6 + 4); [reflexivity | reflexivity].
 qed.