aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/mod_checking.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-10-01 13:32:47 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2015-10-02 15:54:13 +0200
commitc1630c9dcdf91dc965b3c375d68e3338fb737531 (patch)
treebf77e70bf7f401ff83563f50621712955b7aa618 /checker/mod_checking.ml
parent67bdc25eb69ecd485ae1c8fa2dd71d1933f355d0 (diff)
Univs: update checker
Diffstat (limited to 'checker/mod_checking.ml')
-rw-r--r--checker/mod_checking.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 998e23c6e..78fff1bbe 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -69,7 +69,7 @@ let mk_mtb mp sign delta =
mod_expr = Abstract;
mod_type = sign;
mod_type_alg = None;
- mod_constraints = Univ.Constraint.empty;
+ mod_constraints = Univ.ContextSet.empty;
mod_delta = delta;
mod_retroknowledge = []; }