aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/locusops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/locusops.mli')
-rw-r--r--pretyping/locusops.mli4
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