aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/term.mli
diff options
context:
space:
mode:
Diffstat (limited to 'checker/term.mli')
-rw-r--r--checker/term.mli7
1 files changed, 0 insertions, 7 deletions
diff --git a/checker/term.mli b/checker/term.mli
index 4993e0718..127fc113d 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -55,10 +55,3 @@ val destArity : constr -> arity
val isArity : constr -> bool
val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
val eq_constr : constr -> constr -> bool
-
-(* Validation *)
-val val_sortfam : Validate.func
-val val_sort : Validate.func
-val val_constr : Validate.func
-val val_rctxt : Validate.func
-val val_nctxt : Validate.func