diff options
Diffstat (limited to 'pretyping/locusops.mli')
-rw-r--r-- | pretyping/locusops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index bd4df6edd..ddf615033 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -34,5 +34,5 @@ val is_nowhere : 'a clause_expr -> bool (** Clause conversion functions, parametrized by a hyp enumeration function *) -val simple_clause_of : (unit -> identifier list) -> clause -> simple_clause -val concrete_clause_of : (unit -> identifier list) -> clause -> concrete_clause +val simple_clause_of : (unit -> Id.t list) -> clause -> simple_clause +val concrete_clause_of : (unit -> Id.t list) -> clause -> concrete_clause |