diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-18 16:35:15 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-18 16:35:15 +0000 |
| commit | 2a451f1809389beb123985d746f2e8febd46832e (patch) | |
| tree | 0bedd2eb88e2ec865070b4757546a4ec4a7fbf6b /checker | |
| parent | 1c98af511e3cdc84c97bfc615a4c012059539d4f (diff) | |
Univ.constraints made fully abstract instead of being a Set of abstract stuff
No need to tell the world about the fact that constraints are
implemented via caml's Set. Other modules just need to know about
the empty and union functions (and addition functions "enforce_geq"
and "enforce_eq" that were already there).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13725 85f007b7-540e-0410-9357-904b9bb8a0f7
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 8c23a7e46..d960e2a7c 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 5de03b16d..1e773df65 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 78408c68c..30149331e 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 c37f371f5..5226db534 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 |