comments syntax changed

[helm.git] / helm / matita / tests / comments.ma

diff --git a/helm/matita/tests/comments.ma b/helm/matita/tests/comments.ma
index 52c6d84764b035b19732ebdf68abb88fd2b87de4..baf461d9a6f6ab675d305afdece057327e642a77 100644 (file)
--- a/helm/matita/tests/comments.ma
+++ b/helm/matita/tests/comments.ma
@@ -29,11 +29,11 @@ theorem a:0=0.
 
 %% questo lo si vuole tenere anche dopo la hint
 hint.
-**)
-apply cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1). 
-
+*)
+reflexivity.
 (* commenti che non devono essere colorati perche'
    non c'e' nulla di eseguibile dopo di loro
 *)
+qed.
 
 %% EOF