diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 7 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 8 |
3 files changed, 10 insertions, 7 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 996e2b6af0..7a9bbd92cf 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -348,8 +348,11 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = (snd (Evd.universe_context ~names:[] ~extensible:true evd')) in - let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in + let univs = + let poly = Flags.is_universe_polymorphism () in + Evd.const_univ_entry ~poly evd' + in + let ce = Declare.definition_entry ~univs value in ignore( Declare.declare_constant name diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 829556a71e..87609296bc 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(None, List.map snd recsl)) + (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 3089ec4708..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 = (snd (Evd.universe_context ~names:[] ~extensible:true 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 |