diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/environ.ml | 2 | ||||
| -rw-r--r-- | checker/indtypes.ml | 2 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 8 | ||||
| -rw-r--r-- | checker/typeops.ml | 2 |
4 files changed, 7 insertions, 7 deletions
diff --git a/checker/environ.ml b/checker/environ.ml index 8c23a7e46f..d960e2a7cb 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -98,7 +98,7 @@ let named_type id env = (* Universe constraints *) let add_constraints c env = - if c == Constraint.empty then + if c == empty_constraint then env else let s = env.env_stratification in diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 5de03b16d5..1e773df65c 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -176,7 +176,7 @@ let check_predicativity env s small level = Type u, _ -> let u' = fresh_local_univ () in let cst = - merge_constraints (enforce_geq u' u Constraint.empty) + merge_constraints (enforce_geq u' u empty_constraint) (universes env) in if not (check_geq cst u' level) then failwith "impredicative Type inductive type" diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 78408c68cf..30149331ef 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -21,8 +21,8 @@ let refresh_arity ar = Sort (Type u) when not (Univ.is_univ_variable u) -> let u' = Univ.fresh_local_univ() in mkArity (ctxt,Type u'), - Univ.enforce_geq u' u Univ.Constraint.empty - | _ -> ar, Univ.Constraint.empty + Univ.enforce_geq u' u Univ.empty_constraint + | _ -> ar, Univ.empty_constraint let check_constant_declaration env kn cb = Flags.if_verbose msgnl (str " checking cst: " ++ prcon kn); @@ -247,12 +247,12 @@ and check_module env mp mb = {typ_mp=mp; typ_expr=sign; typ_expr_alg=None; - typ_constraints=Univ.Constraint.empty; + typ_constraints=Univ.empty_constraint; typ_delta = mb.mod_delta;} {typ_mp=mp; typ_expr=mb.mod_type; typ_expr_alg=None; - typ_constraints=Univ.Constraint.empty; + typ_constraints=Univ.empty_constraint; typ_delta = mb.mod_delta;}; and check_structure_field env mp lab res = function diff --git a/checker/typeops.ml b/checker/typeops.ml index c37f371f56..5226db5349 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -255,7 +255,7 @@ let refresh_arity env ar = match hd with Sort (Type u) when not (is_univ_variable u) -> let u' = fresh_local_univ() in - let env' = add_constraints (enforce_geq u' u Constraint.empty) env in + let env' = add_constraints (enforce_geq u' u empty_constraint) env in env', mkArity (ctxt,Type u') | _ -> env, ar |