diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/misctypes.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 91fdf3829..6ee44215c 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -40,9 +40,9 @@ type 'id move_location = type sort_info = string option type glob_sort = GProp | GSet | GType of sort_info -(** A synonym of [int], also defined in Term *) +(** A synonym of [Evar.t], also defined in Term *) -type existential_key = int +type existential_key = Evar.t (** Case style, shared with Term *) |