summaryrefslogtreecommitdiff
path: root/src/Pure.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Pure.ml2
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;
}