aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/values.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-23 17:26:38 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-23 17:26:42 +0100
commitb5f0c9f7cd409ab42f034309eedb7eb0247e05cf (patch)
treece2a5e4db982f4522788cb6e3e36900ac5da0990 /checker/values.ml
parente58beb05c80140fbc5f1d0646ece48675370fdc7 (diff)
Vi2vo: fix handling of univ constraints coming from the body
Diffstat (limited to 'checker/values.ml')
-rw-r--r--checker/values.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/values.ml b/checker/values.ml
index 08cb08be8..ea3df47f5 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -109,7 +109,7 @@ let v_cstrs =
let v_instance = Annot ("instance", Array v_level)
let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|]
-let v_context_set = v_tuple "universe_context_set" [|v_set v_level;v_cstrs|]
+let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
(** kernel/term *)