diff options
Diffstat (limited to 'src/property.mli')
| -rw-r--r-- | src/property.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/property.mli b/src/property.mli index 66a732b9..2d366fa0 100644 --- a/src/property.mli +++ b/src/property.mli @@ -52,6 +52,7 @@ $counterexample pragmas. *) open Ast +open Ast_defs open Ast_util open Type_check @@ -66,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 @@ -86,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 |