diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-28 13:20:41 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-28 13:20:41 +0000 |
| commit | f19a9d9d3a410fda982b2cf9154da5774f9ec84f (patch) | |
| tree | 23e166d4564ec1382afb60ec0d03e976dcaff377 /plugins/funind/indfun.ml | |
| parent | c7fb97fd915a732e1d91ca59fd635c95235052ce (diff) | |
Remove the "Boxed" syntaxes and the const_entry_boxed field
According to B. Gregoire, this stuff is obsolete. Fine control
on when to launch the VM in conversion problems is now provided
by VMcast. We were already almost never boxing definitions anymore
in stdlib files.
"(Un)Boxed Definition foo" will now trigger a parsing error,
same with Fixpoint. The option "(Un)Set Boxed Definitions"
aren't there anymore, but tolerated (as no-ops), since unknown
options raise a warning instead of an error by default.
Some more cleaning could be done in the vm.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |