diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 5 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 3 |
3 files changed, 4 insertions, 8 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 0cc5af99f2..1d089409b0 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -382,9 +382,7 @@ let generate_functional_principle let ce = { const_entry_body = value; const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() - } + const_entry_opaque = false } in ignore( Declare.declare_constant diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index f23fcd6134..e571803273 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -351,14 +351,13 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in let ce,imps = - Command.interp_definition - (Flags.boxed_definitions ()) bl None body (Some ret_type) + Command.interp_definition bl None body (Some ret_type) in Command.declare_definition fname (Decl_kinds.Global,Decl_kinds.Definition) ce imps (fun _ _ -> ()) | _ -> - Command.do_fixpoint fixpoint_exprl (Flags.boxed_definitions()) + Command.do_fixpoint fixpoint_exprl let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 3ab9d58d50..feff5d67c6 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1136,8 +1136,7 @@ let (declare_fun : identifier -> logical_kind -> constr -> global_reference) = fun f_id kind value -> let ce = {const_entry_body = value; const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = true} in + const_entry_opaque = false } in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) = |