aboutsummaryrefslogtreecommitdiff
path: root/checker/mod_checking.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/mod_checking.ml')
-rw-r--r--checker/mod_checking.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 1cf07e7cc7..1bc5891517 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -13,7 +13,6 @@ let set_indirect_accessor f = get_proof := f
let indirect_accessor = {
Opaqueproof.access_proof = (fun dp n -> !get_proof dp n);
- Opaqueproof.access_constraints = (fun _ _ -> assert false);
}
let check_constant_declaration env kn cb =