]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/proofEngineTypes.ml
- reimplemented tacticChaser and friends in term of Metadata module and friends
[helm.git] / helm / ocaml / tactics / proofEngineTypes.ml
index 8d1def22ebd7bd360df377967a3bd85885fd0355..b4992aca3496420c9f1277a50b9065aed36985c5 100644 (file)
@@ -67,7 +67,9 @@ let apply_tactic t status =
   let saved_univ = CicUniv.get_working() in
   try 
     t status
-  with Fail s -> CicUniv.set_working saved_univ; raise (Fail s)
+  with Fail s ->
+    CicUniv.set_working saved_univ;
+    raise (Fail s)
 
   (** constraint: the returned value will always be constructed by Cic.Name **)
 type mk_fresh_name_type =