diff options
Diffstat (limited to 'src/property.mli')
| -rw-r--r-- | src/property.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/property.mli b/src/property.mli index bba1f638..2d366fa0 100644 --- a/src/property.mli +++ b/src/property.mli @@ -67,7 +67,7 @@ open Type_check where prop_type is either "counterexample" or "property" and the location loc is the location that was attached to the pragma *) -val find_properties : 'a defs -> (string * string * l * 'a val_spec) Bindings.t +val find_properties : 'a ast -> (string * string * l * 'a val_spec) Bindings.t (** For a property @@ -87,7 +87,7 @@ val find_properties : 'a defs -> (string * string * l * 'a val_spec) Bindings.t generation/proving we want to ensure that inputs outside the constraints of the function are ignored. *) -val rewrite : tannot defs -> tannot defs +val rewrite : tannot ast -> tannot ast type event = Overflow | Assertion | Assumption | Match | Return |