diff options
Diffstat (limited to 'src/Pure.ml')
| -rw-r--r-- | src/Pure.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Pure.ml b/src/Pure.ml index b7a61ab0..0016aedb 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -227,6 +227,7 @@ type inst_fun_sig = { inputs : ty list; outputs : ty list } type fun_def = { def_id : FunDefId.id; + back_id : T.RegionGroupId.id option; basename : name; (** The "base" name of the function. |