Merge pull request #3374 from mtzguido/idinfo

Tactics: restoring ID info table on a failure
FStarLang · Aug 14, 2024 · 8a208d6 · 8a208d6
2 parents 608c8c2 + 50ed7b8
commit 8a208d6
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Monad.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Monad.ml
diff --git a/src/tactics/FStar.Tactics.Monad.fst b/src/tactics/FStar.Tactics.Monad.fst
@@ -169,13 +169,15 @@ let fail msg = fail_doc [text msg]
 
 let catch (t : tac 'a) : tac (either exn 'a) =
     mk_tac (fun ps ->
+            let idtable = !ps.main_context.identifier_info in
             let tx = UF.new_transaction () in
             match run t ps with
             | Success (a, q) ->
                 UF.commit tx;
                 Success (Inr a, q)
             | Failed (m, q) ->
                 UF.rollback tx;
+                ps.main_context.identifier_info := idtable;
                 let ps = { ps with freshness = q.freshness } in //propagate the freshness even on failures
                 Success (Inl m, ps)
            )