diff options
| author | letouzey | 2011-01-28 13:20:41 +0000 |
|---|---|---|
| committer | letouzey | 2011-01-28 13:20:41 +0000 |
| commit | f19a9d9d3a410fda982b2cf9154da5774f9ec84f (patch) | |
| tree | 23e166d4564ec1382afb60ec0d03e976dcaff377 /plugins/funind | |
| 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')
| -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) = |