diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-07 16:33:47 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 14:50:47 +0200 |
commit | 0d9a91113c4112eece0680e433f435fdfb39ea4b (patch) | |
tree | cf90d290a92c02a2297b3a13b77190db9aa4db70 /engine/universes.ml | |
parent | b5ad6a80107f196fa8ffcc4f5dff58bea8c4f70e (diff) |
Getting rid of simple calls to AUContext.instance.
This function breaks the abstraction barrier of abstract universe contexts,
as it provides a way to observe the bound names of such a context. We remove
all the uses that can be easily get rid of with the current API.
Diffstat (limited to 'engine/universes.ml')
-rw-r--r-- | engine/universes.ml | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index 28058aeed..5df02c8a9 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -282,8 +282,8 @@ let new_Type dp = mkType (new_univ dp) let new_Type_sort dp = Type (new_univ dp) let fresh_universe_instance ctx = - Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ())) - (AUContext.instance ctx) + let init _ = new_univ_level (Global.current_dirpath ()) in + Instance.of_array (Array.init (AUContext.size ctx) init) let fresh_instance_from_context ctx = let inst = fresh_universe_instance ctx in @@ -292,18 +292,17 @@ let fresh_instance_from_context ctx = let fresh_instance ctx = let ctx' = ref LSet.empty in - let inst = - Instance.subst_fn (fun v -> - let u = new_univ_level (Global.current_dirpath ()) in - ctx' := LSet.add u !ctx'; u) - (AUContext.instance ctx) + let init _ = + let u = new_univ_level (Global.current_dirpath ()) in + ctx' := LSet.add u !ctx'; u + in + let inst = Instance.of_array (Array.init (AUContext.size ctx) init) in !ctx', inst let existing_instance ctx inst = let () = - let a1 = Instance.to_array inst - and a2 = Instance.to_array (AUContext.instance ctx) in - let len1 = Array.length a1 and len2 = Array.length a2 in + let len1 = Array.length (Instance.to_array inst) + and len2 = AUContext.size ctx in if not (len1 == len2) then CErrors.user_err ~hdr:"Universes" (str "Polymorphic constant expected " ++ int len2 ++ |