]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/tests/clear.ma
ocaml 3.09 transition
[helm.git] / helm / matita / tests / clear.ma
index 71457ae2c295e980bf85673bc3b25b8fefa07a57..9f1655b597fc6da3dc6b763334075a4e7ae9eb12 100644 (file)
@@ -22,9 +22,9 @@ theorem stupid:
   \forall a: True.
   \forall b: 0 = 0.
   0 = 0.
-intros 1 [H] .
+intros 1 (H).
 clear H.
-intros 1 [H].
+intros 1 (H).
 exact H.
 qed.