diff options
Diffstat (limited to 'plugins/funind')
| -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 |
3 files changed, 3 insertions, 0 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));; |