diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-18 17:22:24 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:23:41 +0100 |
commit | 34d85e1e899f8a045659ccc53bfd6a1f5104130b (patch) | |
tree | ed176f6f7d0d47802d5c4e1879cd2eb35232df46 /plugins/funind/recdef.ml | |
parent | 58c0784745f8b2ba7523f246c4611d780c9f3f70 (diff) |
Use Entries.constant_universes_entry more.
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
Diffstat (limited to 'plugins/funind/recdef.ml')
-rw-r--r-- | plugins/funind/recdef.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 320f7c7f3..b0a76137b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -66,8 +66,8 @@ let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in locate (make_qualid dp (Id.of_string s)) -let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value = - let ce = definition_entry ~univs:ctx value (*FIXME *) in +let declare_fun f_id kind ?univs value = + let ce = definition_entry ?univs value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None))) @@ -1556,8 +1556,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let ctx = Evd.to_universe_context evm in - declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res + let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in + declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res in (* Refresh the global universes, now including those of _F *) let evm = Evd.from_env (Global.env ()) in |