diff options
| author | Sidney Congard | 2022-07-18 16:27:00 +0200 |
|---|---|---|
| committer | Sidney Congard | 2022-07-18 16:27:23 +0200 |
| commit | f9b324be57708e9496ca6e9ac0b7e68ffd9e7108 (patch) | |
| tree | f81bdfe1ddad63938df046ca361dcba2dfea6683 /src/Pure.ml | |
| parent | 8f14d69ae6683e58e1387ffe38ca3612e0530465 (diff) | |
Address much stuff of the PR, throw exceptions at remaining places
Diffstat (limited to 'src/Pure.ml')
| -rw-r--r-- | src/Pure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Pure.ml b/src/Pure.ml index b3be2040..5244b0bc 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -575,6 +575,6 @@ type fun_decl = { (to identify the forward/backward functions) later. *) signature : fun_sig; - is_global : bool; + is_global_body : bool; body : fun_body option; } |