X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Ftests.ma;h=344ac7c337fb48902a48fdf8f6ef1c7e92f17500;hb=11e495dda047bcdfa4267c06cad2d074fcffe3e3;hp=e07e44092ed477102615aa60ba8c908040bb3020;hpb=8cefaf42402a475f7a541cf492cbac04b5d02c16;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/compiler/tests.ma b/helm/software/matita/contribs/assembly/compiler/tests.ma
index e07e44092..344ac7c33 100755
--- a/helm/software/matita/contribs/assembly/compiler/tests.ma
+++ b/helm/software/matita/contribs/assembly/compiler/tests.ma
@@ -225,4 +225,5 @@ lemma pippo : ∃b.preast_to_ast parsingResult = Some ? b.
  exists;
  [ apply (match preast_to_ast parsingResult with [ None ⇒ AST_ROOT (AST_NO_DECL O empty_env []) | Some x ⇒ x]);
  | reflexivity
- ].
+ ]
+qed.