diff options
| author | Alasdair Armstrong | 2017-11-16 15:26:31 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-11-16 15:26:31 +0000 |
| commit | 6921b3107088f43b38eadcd841384deff00e340e (patch) | |
| tree | db28456bfd14b76aac2776920ec402b83a086625 /src/pretty_print_lem.ml | |
| parent | 9a5bd2079a5fe42bde4c207851c2c3b1fd0035b7 (diff) | |
Remove unused Typ_wild constructor
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index c32212a6..22f210e8 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -191,7 +191,6 @@ let rec orig_nexp (Nexp_aux (nexp, l)) = let rec lem_nexps_of_typ sequential mwords (Typ_aux (t,_)) = let trec = lem_nexps_of_typ sequential mwords in match t with - | Typ_wild | Typ_id _ -> NexpSet.empty | Typ_var kid -> NexpSet.singleton (orig_nexp (nvar kid)) | Typ_fn (t1,t2,_) -> NexpSet.union (trec t1) (trec t2) @@ -294,7 +293,6 @@ let doc_typ_lem, doc_atomic_typ_lem = then string "register" else*) doc_id_lem_type id | Typ_var v -> doc_var v - | Typ_wild -> underscore | Typ_app _ | Typ_tup _ | Typ_fn _ -> (* exhaustiveness matters here to avoid infinite loops * if we add a new Typ constructor *) @@ -322,7 +320,6 @@ let doc_typ_lem, doc_atomic_typ_lem = a bitvector; for other types of vectors, the length is not pretty-printed in the type, and the start index is never pretty-printed in vector types. *) let rec contains_t_pp_var mwords (Typ_aux (t,a) as typ) = match t with - | Typ_wild -> true | Typ_id _ -> false | Typ_var _ -> true | Typ_exist _ -> true @@ -423,7 +420,6 @@ let doc_typquant_lem (TypQ_aux(tq,_)) vars_included typ = match tq with approach will do for now. *) let rec typeclass_nexps (Typ_aux(t,_)) = match t with -| Typ_wild | Typ_id _ | Typ_var _ -> NexpSet.empty |