From abaf651b3d3ff230cac0b85bcd2cf70461400d05 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 12 Dec 2008 14:59:39 +0000 Subject: [PATCH] ... --- helm/software/matita/contribs/assembly/compiler/tests.ma | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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. -- 2.39.2