]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/matitaExcPp.ml
acic_procedural and tactics removed
[helm.git] / matita / matita / matitaExcPp.ml
index 04bdd6a3871af183948a1a81e68c7dc83c2a3d21..260ac2f29ae38cf7e97de5c22f56f99108d36322 100644 (file)
@@ -133,10 +133,7 @@ let rec to_string =
       None,
       sprintf "format/version mismatch for file '%s', please recompile it'"
         fname
-  | ProofEngineTypes.Fail msg -> None, "Tactic error: " ^ Lazy.force msg
   | Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s
-  | ProofEngineHelpers.Bad_pattern msg ->
-     None, "Bad pattern: " ^ Lazy.force msg
   | CicRefine.RefineFailure msg
   | CicRefine.AssertFailure msg ->
      None, "Refiner error: " ^ Lazy.force msg