diff options
| author | Son Ho | 2022-09-22 17:52:27 +0200 |
|---|---|---|
| committer | Son Ho | 2022-09-22 17:52:27 +0200 |
| commit | c8ccd864e1fa6de3241d9dba184cf8ee4101e421 (patch) | |
| tree | 3651d70ab5a9236d9b7c4ae85520d74442fa964c /src/Pure.ml | |
| parent | f106fd4ad0a221611c840bf0af0b1c2ff23f3d0f (diff) | |
Make minor cleanup
Diffstat (limited to '')
| -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 5244b0bc..ced56c6a 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_body : bool; + is_global_decl_body : bool; body : fun_body option; } |