diff options
Diffstat (limited to 'src/ExtractToFStar.ml')
| -rw-r--r-- | src/ExtractToFStar.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 9766ddaf..b85c146b 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -902,7 +902,10 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) | AdtCons adt_cons_id -> extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args | Proj proj -> - extract_field_projector ctx fmt inside app proj qualif.type_args args) + extract_field_projector ctx fmt inside app proj qualif.type_args args + (* TODO | Global global_id -> + extract_global_ref ctx fmt inside global_id*) + ) | _ -> (* "Regular" expression *) (* Open parentheses *) |