fix

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index c5d36ee48359c9354b4896a3b6311759a8ed3716..7e7ac5641e3ea71b3b2c42f854d9455e0375f192 100644 (file)
--- 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 *)