From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 24 May 2005 10:09:08 +0000 (+0000)
Subject: fix
X-Git-Tag: single_binding~18
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4faa2b8428b153e5e80c758880236178399fa0fe;p=helm.git

fix
---

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 *)