summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-11-05 18:04:51 +0000
committerAlasdair Armstrong2019-11-05 18:39:21 +0000
commit1edd0e73a7d19904639341fd360fff5fa3ff4fec (patch)
treeedcbd6e3b3ce6ed8b8cde739cdd6a502af480ac3 /src/rewrites.ml
parentf42e1a8adbf220bd03862bb08ca5103b6e1cde09 (diff)
Make sure we correctly forbid recursive datatypes that we don't want to support
Ensure we give a nice error message that explains that recursive types are forbidden ``` Type error: [struct_rec.sail]:3:10-11 3 | field : S | ^ | Undefined type S | This error was caused by: | [struct_rec.sail]:2:0-4:1 | 2 |struct S = { | |^----------- | 4 |} | |^ | | Recursive types are not allowed ``` The theorem prover backends create a special register_value union that can be recursive, so we make sure to special case that.
Diffstat (limited to 'src/rewrites.ml')
0 files changed, 0 insertions, 0 deletions