diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 429aba4f75..09fe64d77b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -188,10 +188,10 @@ let map_universes f env = let add_constraints c env = if Univ.Constraint.is_empty c then env - else map_universes (Univ.merge_constraints c) env + else map_universes (UGraph.merge_constraints c) env let check_constraints c env = - Univ.check_constraints c env.env_stratification.env_universes + UGraph.check_constraints c env.env_stratification.env_universes let push_constraints_to_env (_,univs) env = add_constraints univs env @@ -199,19 +199,19 @@ let push_constraints_to_env (_,univs) env = let add_universes strict ctx g = let g = Array.fold_left (* Be lenient, module typing reintroduces universes and constraints due to includes *) - (fun g v -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g) + (fun g v -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) g (Univ.Instance.to_array (Univ.UContext.instance ctx)) in - Univ.merge_constraints (Univ.UContext.constraints ctx) g + UGraph.merge_constraints (Univ.UContext.constraints ctx) g let push_context ?(strict=false) ctx env = map_universes (add_universes strict ctx) env let add_universes_set strict ctx g = let g = Univ.LSet.fold - (fun v g -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g) + (fun v g -> try UGraph.add_universe v strict g with UGraph.AlreadyDeclared -> g) (Univ.ContextSet.levels ctx) g - in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g + in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g let push_context_set ?(strict=false) ctx env = map_universes (add_universes_set strict ctx) env @@ -602,7 +602,10 @@ let dispatch = Array.init 31 (fun n -> mkConstruct (digit_ind, nth_digit_plus_one i (30-n))) in - mkApp(mkConstruct(ind, 1), array_of_int tag) + (* We check that no bit above 31 is set to one. This assertion used to + fail in the VM, and led to conversion tests failing at Qed. *) + assert (Int.equal (tag lsr 31) 0); + mkApp(mkConstruct(ind, 1), array_of_int tag) in (* subfunction which dispatches the compiling information of an |