Skip to content

Commit

Permalink
account for lids too, in free_vars
Browse files Browse the repository at this point in the history
  • Loading branch information
nikswamy committed Aug 15, 2023
1 parent dbc012b commit a3158d4
Show file tree
Hide file tree
Showing 2 changed files with 12 additions and 9 deletions.
12 changes: 7 additions & 5 deletions ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

9 changes: 5 additions & 4 deletions src/tosyntax/FStar.ToSyntax.ToSyntax.fst
Original file line number Diff line number Diff line change
Expand Up @@ -325,10 +325,11 @@ and free_vars tvars_only env t = match (unparen t).tm with
else (
let ids = Ident.ids_of_lid x in
match ids with
| [x] -> ( //unqualified name
match Env.try_lookup_id env x with
| None -> [x]
| _ -> []
| [id] -> ( //unqualified name
if None? (Env.try_lookup_id env id)
&& None? (Env.try_lookup_lid env x)
then [id]
else []
)
| _ -> []
)
Expand Down

0 comments on commit a3158d4

Please sign in to comment.