diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 1 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 1 | ||||
| -rw-r--r-- | plugins/subtac/subtac_command.ml | 3 | ||||
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 6 |
6 files changed, 10 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index f37cb3ed03..6df9d574f9 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -381,6 +381,7 @@ let generate_functional_principle (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) let ce = { const_entry_body = value; + const_entry_secctx = None; const_entry_type = None; const_entry_opaque = false } in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 233cdddd7f..dd475315c7 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -158,6 +158,7 @@ let definition_message id = let save with_clean id const (locality,kind) hook = let {const_entry_body = pft; + const_entry_secctx = _; const_entry_type = tpo; const_entry_opaque = opacity } = const in let l,r = match locality with diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c65d3181c3..55ebd31b93 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1131,6 +1131,7 @@ let (value_f:constr list -> global_reference -> constr) = let (declare_fun : identifier -> logical_kind -> constr -> global_reference) = fun f_id kind value -> let ce = {const_entry_body = value; + const_entry_secctx = None; const_entry_type = None; const_entry_opaque = false } in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index d189a4e55c..9d61c06de6 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -158,6 +158,7 @@ let ty c = Typing.type_of (Global.env()) Evd.empty c let decl_constant na c = mkConst(declare_constant (id_of_string na) (DefinitionEntry { const_entry_body = c; + const_entry_secctx = None; const_entry_type = None; const_entry_opaque = true }, IsProof Lemma)) diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index f02e83ad1a..ecae6759f0 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -325,7 +325,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ce = - { const_entry_body = Evarutil.nf_evar !isevars body; + { const_entry_body = Evarutil.nf_evar !isevars body; + const_entry_secctx = None; const_entry_type = Some ty; const_entry_opaque = false } in diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index a719a9f9af..64d9f72cae 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -248,6 +248,7 @@ let declare_definition prg = let (local, kind) = prg.prg_kind in let ce = { const_entry_body = body; + const_entry_secctx = None; const_entry_type = Some typ; const_entry_opaque = false } in @@ -347,6 +348,7 @@ let declare_obligation prg obl body = let opaque = if get_proofs_transparency () then false else opaque in let ce = { const_entry_body = body; + const_entry_secctx = None; const_entry_type = Some ty; const_entry_opaque = opaque } in @@ -661,8 +663,8 @@ let admit_obligations n = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,None), - IsAssumption Conjectural) + let kn = Declare.declare_constant x.obl_name + (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural) in assumption_message x.obl_name; obls.(i) <- { x with obl_body = Some (mkConst kn) } |