From 4faa2b8428b153e5e80c758880236178399fa0fe Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 24 May 2005 10:09:08 +0000 Subject: [PATCH] fix --- helm/matita/matitaEngine.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index c5d36ee48..7e7ac5641 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -150,8 +150,11 @@ let eval_command status cmd = CicTypeChecker.typecheck_mutual_inductive_defs uri (types, [], leftno) CicUniv.empty_ugraph in + let status = MatitaSync.add_inductive_def - ~uri ~types ~params:[] ~leftno ~ugraph status; + ~uri ~types ~params:[] ~leftno ~ugraph status + in + {status with proof_status = No_proof } | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) -> let uri = UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") @@ -181,7 +184,8 @@ let eval_command status cmd = "metasenv not empty while giving a definition with body"; let body = CicMetaSubst.apply_subst subst body in let ty = CicMetaSubst.apply_subst subst ty in - MatitaSync.add_constant ~uri ~body ~ty ~ugraph status + let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in + {status with proof_status = No_proof} | TacticAst.Theorem (_, _, None, _, _) -> command_error "The grammas should avoid having unnamed theorems!" | TacticAst.Coercion (loc, term) -> assert false (** TODO *) -- 2.39.2