Commit 51d931e
- lib/common/Pulse.Lib.Core.fsti+11
- lib/core/Pulse.Lib.Core.fst+2
- lib/pulse/lib/Pulse.Lib.Array.Core.fsti+1
- lib/pulse/lib/Pulse.Lib.Reference.Array.fsti+1
- lib/pulse/lib/Pulse.Lib.Reference.fsti+3
- src/checker/Pulse.Checker.Defer.fst+75
- src/checker/Pulse.Checker.Defer.fsti+32
- src/checker/Pulse.Checker.ImpureSpec.fst+4-1
- src/checker/Pulse.Checker.fst+4
- src/checker/Pulse.ElimGoto.fst+14
- src/checker/Pulse.Extract.Main.fst+12
- src/checker/Pulse.Syntax.Base.fst+4
- src/checker/Pulse.Syntax.Base.fsti+5
- src/checker/Pulse.Syntax.Builder.fst+1
- src/checker/Pulse.Syntax.Naming.fst+5
- src/checker/Pulse.Syntax.Naming.fsti+9
- src/checker/Pulse.Syntax.Printer.fst+9
- src/checker/Pulse.Typing.FV.fst+6-1
- src/ml/PulseSyntaxExtension_Parser.ml+1
- src/ml/PulseSyntaxExtension_SyntaxWrapper.ml+3
- src/ml/pulseparser.mly+3-1
- src/syntax_extension/PulseSyntaxExtension.Desugar.fst+10
- src/syntax_extension/PulseSyntaxExtension.Sugar.fst+17
- src/syntax_extension/PulseSyntaxExtension.SyntaxWrapper.fsti+1
- test/Defer.fst+21
- test/Defer.ml.expected+14
0 commit comments