diff options
Diffstat (limited to 'interp/reserve.mli')
| -rw-r--r-- | interp/reserve.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/reserve.mli b/interp/reserve.mli index a72aa8ec9..3bcba719c 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -9,7 +9,8 @@ open Util open Names open Rawterm +open Topconstr -val declare_reserved_type : identifier located -> rawconstr -> unit -val find_reserved_type : identifier -> rawconstr +val declare_reserved_type : identifier located -> aconstr -> unit +val find_reserved_type : identifier -> aconstr val anonymize_if_reserved : name -> rawconstr -> rawconstr |