summaryrefslogtreecommitdiff
path: root/src/spec_analysis.ml
diff options
context:
space:
mode:
authorPeter Sewell2018-07-27 18:57:02 +0100
committerPeter Sewell2018-07-27 18:57:02 +0100
commit3755e6701a9286677fd2f4ca40a16305b360f9d9 (patch)
tree67766e537db5bb8dbfc6b59432b2786a88b76be3 /src/spec_analysis.ml
parent2a35c6b9e1cfac8ce34ef6fa7c264cfea4139002 (diff)
parente4af7c3090c93a129e99dd75f2a20d5a9d2f6920 (diff)
Merge branch 'sail2' of github.com:rems-project/sail into sail2
Diffstat (limited to 'src/spec_analysis.ml')
-rw-r--r--src/spec_analysis.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 9481d6b1..b459610d 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -105,7 +105,8 @@ and free_type_names_t_args consider_var targs =
nameset_bigunion (List.map (free_type_names_t_arg consider_var) targs)
-let rec free_type_names_tannot consider_var = function
+let rec free_type_names_tannot consider_var tannot =
+ match Type_check.destruct_tannot tannot with
| None -> mt
| Some (_, t, _) -> free_type_names_t consider_var t