From a5feb9687819c5e7ef0db6e7b74d0e236a296674 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 21:01:57 +0200 Subject: Separate checking univ_decls and obtaining universe binder names. --- plugins/funind/recdef.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/recdef.ml') diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 3089ec4708..63896bb560 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1556,7 +1556,7 @@ 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 = (snd (Evd.universe_context ~names:[] ~extensible:true evm)) in + let ctx = Evd.universe_context ~names:[] ~extensible:true evm in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res in (* Refresh the global universes, now including those of _F *) -- cgit v1.2.3 From 60770e86f4ec925fce52ad3565a92beb98d253c1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 22:21:46 +0200 Subject: Stop exposing UState.universe_context and its Evd wrapper. We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former). --- plugins/funind/recdef.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/recdef.ml') diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 63896bb560..320f7c7f31 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1556,7 +1556,7 @@ 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.universe_context ~names:[] ~extensible:true evm in + let ctx = Evd.to_universe_context evm in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res in (* Refresh the global universes, now including those of _F *) -- cgit v1.2.3 From 34d85e1e899f8a045659ccc53bfd6a1f5104130b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 17:22:24 +0200 Subject: 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. --- plugins/funind/recdef.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/funind/recdef.ml') diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 320f7c7f31..b0a76137b7 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 -- cgit v1.2.3