diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index f23fcd613..e57180327 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 |