diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-28 19:26:21 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-17 18:46:09 +0200 |
commit | a51dda2344679dc6d9145f3f34acad29721f6c75 (patch) | |
tree | c9ed50095ae459dabd97d9571566647439cf5269 /plugins/funind/functional_principles_types.ml | |
parent | b0ef649660542ae840ea945d7ab4f1f3ae7b85cd (diff) |
Split off Universes functions dealing with generating new universes.
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index dc0f240bd..a158fc8ff 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -689,7 +689,7 @@ let build_case_scheme fa = let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in let sorts = (fun (_,_,x) -> - Universes.new_sort_in_family x + UnivGen.new_sort_in_family x ) fa in |