diff options
71 files changed, 143 insertions, 239 deletions
@@ -17,6 +17,8 @@ Vernacular commands - When the output file of "Print Universes" ends in ".dot" or ".gv", the universe graph is printed in the DOT language, and can be processed by Graphviz tools. +- The undocumented and obsolete option "Set/Unset Boxed Definitions" has + been removed, as well as syntaxes like "Boxed Fixpoint foo". Libraries diff --git a/Makefile.build b/Makefile.build index b2b311a4f..d14152842 100644 --- a/Makefile.build +++ b/Makefile.build @@ -63,14 +63,13 @@ READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary VALIDATE= COQ_XML= # is "-xml" when building XML library VM= # is "-no-vm" to not use the vm" -UNBOXEDVALUES= # is "-unboxed-values" to use unboxed values TIMECMD= # is "'time -p'" to get compilation time of .v # NB: variable TIME, if set, is the formatting string for unix command 'time'. # For instance: # TIME="%C (%U user, %S sys, %e total, %M maxres)" -COQOPTS=$(COQ_XML) $(VM) $(UNBOXEDVALUES) +COQOPTS=$(COQ_XML) $(VM) BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS) # The SHOW and HIDE variables control whether make will echo complete commands diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 9c00af5df..337b90751 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -714,18 +714,13 @@ let compile env c = Format.print_flush(); *) init_code,!fun_code, Array.of_list fv -let compile_constant_body env body opaque boxed = +let compile_constant_body env body opaque = if opaque then BCconstant else match body with | None -> BCconstant | Some sb -> let body = Declarations.force sb in - if boxed then - let res = compile env body in - let to_patch = to_memory res in - BCdefined(true, to_patch) - else - match kind_of_term body with + match kind_of_term body with | Const kn' -> (* we use the canonical name of the constant*) let con= constant_of_kn (canonical_con kn') in @@ -733,7 +728,7 @@ let compile_constant_body env body opaque boxed = | _ -> let res = compile env body in let to_patch = to_memory res in - BCdefined (false, to_patch) + BCdefined to_patch (* spiwack: additional function which allow different part of compilation of the diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index bf9c0be26..403c1c7b5 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -10,8 +10,8 @@ val compile : env -> constr -> bytecodes * bytecodes * fv (** init, fun, fv *) val compile_constant_body : - env -> constr_substituted option -> bool -> bool -> body_code - (** opaque *) (* boxed *) + env -> constr_substituted option -> bool -> body_code + (** opaque *) (** spiwack: this function contains the information needed to perform diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 1138031c7..277b343b2 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -331,12 +331,12 @@ let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv type body_code = - | BCdefined of bool * to_patch + | BCdefined of to_patch | BCallias of constant | BCconstant let subst_body_code s = function - | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp) + | BCdefined tp -> BCdefined (subst_to_patch s tp) | BCallias kn -> BCallias (fst (subst_con s kn)) | BCconstant -> BCconstant @@ -348,11 +348,6 @@ let force = force subst_body_code let subst_to_patch_subst = subst_substituted -let is_boxed tps = - match force tps with - | BCdefined(b,_) -> b - | _ -> false - let to_memory (init_code, fun_code, fv) = init(); emit init_code; diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index a8ecc82b4..43cebb474 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -22,7 +22,7 @@ type to_patch = emitcodes * (patch list) * fv val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch type body_code = - | BCdefined of bool*to_patch + | BCdefined of to_patch | BCallias of constant | BCconstant @@ -33,8 +33,6 @@ val from_val : body_code -> to_patch_substituted val force : to_patch_substituted -> body_code -val is_boxed : to_patch_substituted -> bool - val subst_to_patch_subst : Mod_subst.substitution -> to_patch_substituted -> to_patch_substituted val to_memory : bytecodes * bytecodes * fv -> to_patch diff --git a/kernel/cooking.ml b/kernel/cooking.ml index e4336683d..d01398841 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -137,5 +137,4 @@ let cook_constant env r = let j = make_judge (force (Option.get body)) typ in Typeops.make_polymorphic_if_constant_for_ind env j in - let boxed = Cemitcodes.is_boxed cb.const_body_code in - (body, typ, cb.const_constraints, cb.const_opaque, boxed,false) + (body, typ, cb.const_constraints, cb.const_opaque, false) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 0f604a4be..09b42d0b1 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -24,7 +24,7 @@ type recipe = { val cook_constant : env -> recipe -> constr_substituted option * constant_type * constraints * bool * bool - * bool + (** {6 Utility functions used in module [Discharge]. } *) diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 983c1f26d..897cbf13a 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -125,10 +125,9 @@ let rec slot_for_getglobal env kn = with NotEvaluated -> let pos = match Cemitcodes.force cb.const_body_code with - | BCdefined(boxed,(code,pl,fv)) -> + | BCdefined(code,pl,fv) -> let v = eval_to_patch env (code,pl,fv) in - if boxed then set_global_boxed kn v - else set_global v + set_global v | BCallias kn' -> slot_for_getglobal env kn' | BCconstant -> set_global (val_of_constant kn) in rk := Some pos; diff --git a/kernel/entries.ml b/kernel/entries.ml index 714da0319..dbf802bb1 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -57,8 +57,7 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; const_entry_type : types option; - const_entry_opaque : bool; - const_entry_boxed : bool} + const_entry_opaque : bool } (* type and the inlining flag *) type parameter_entry = types * bool diff --git a/kernel/entries.mli b/kernel/entries.mli index 2ba306455..d45e2bbdb 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -53,8 +53,7 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; const_entry_type : types option; - const_entry_opaque : bool; - const_entry_boxed : bool } + const_entry_opaque : bool } type parameter_entry = types * bool (*inline flag*) diff --git a/kernel/environ.mli b/kernel/environ.mli index 078d70965..f26d49dde 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -190,8 +190,8 @@ type unsafe_type_judgment = { (** {6 Compilation of global declaration } *) val compile_constant_body : - env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code - (** opaque *) (* boxed *) + env -> constr_substituted option -> bool -> Cemitcodes.body_code + (** opaque *) exception Hyp_not_found diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 5a3dade53..407ae73ca 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -95,7 +95,7 @@ and check_with_aux_def env sign with_decl mp equiv = let cb' = {cb with const_body = body; const_body_code = Cemitcodes.from_val - (compile_constant_body env' body false false); + (compile_constant_body env' body false); const_constraints = cst} in SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst | Some b -> @@ -105,7 +105,7 @@ and check_with_aux_def env sign with_decl mp equiv = let cb' = {cb with const_body = body; const_body_code = Cemitcodes.from_val - (compile_constant_body env' body false false); + (compile_constant_body env' body false); const_constraints = cst} in SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst end diff --git a/kernel/modops.ml b/kernel/modops.ml index 9da2f4962..ce968b40e 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -276,7 +276,7 @@ let strengthen_const env mp_from l cb resolver = const_body = const_subs; const_opaque = false; const_body_code = Cemitcodes.from_val - (compile_constant_body env const_subs false false) + (compile_constant_body env const_subs false) } diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f765dd77e..432460d7d 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -94,11 +94,11 @@ let infer_declaration env dcl = let (j,cst) = infer env c.const_entry_body in let (typ,cst) = constrain_type env j cst c.const_entry_type in Some (Declarations.from_val j.uj_val), typ, cst, - c.const_entry_opaque, c.const_entry_boxed, false + c.const_entry_opaque, false | ParameterEntry (t,nl) -> let (j,cst) = infer env t in None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst, - false, false, nl + false, nl let global_vars_set_constant_type env = function | NonPolymorphicType t -> global_vars_set env t @@ -108,7 +108,7 @@ let global_vars_set_constant_type env = function (fun t c -> Idset.union (global_vars_set env t) c)) ctx ~init:Idset.empty -let build_constant_declaration env kn (body,typ,cst,op,boxed,inline) = +let build_constant_declaration env kn (body,typ,cst,op,inline) = let ids = match body with | None -> global_vars_set_constant_type env typ @@ -117,7 +117,7 @@ let build_constant_declaration env kn (body,typ,cst,op,boxed,inline) = (global_vars_set env (Declarations.force b)) (global_vars_set_constant_type env typ) in - let tps = Cemitcodes.from_val (compile_constant_body env body op boxed) in + let tps = Cemitcodes.from_val (compile_constant_body env body op) in let hyps = keep_hyps env ids in { const_hyps = hyps; const_body = body; diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 628aa9375..500858a59 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -22,10 +22,10 @@ val translate_local_assum : env -> types -> types * Univ.constraints val infer_declaration : env -> constant_entry -> - constr_substituted option * constant_type * constraints * bool * bool * bool + constr_substituted option * constant_type * constraints * bool * bool val build_constant_declaration : env -> 'a -> - constr_substituted option * constant_type * constraints * bool * bool * bool -> + constr_substituted option * constant_type * constraints * bool * bool -> constant_body val translate_constant : env -> constant -> constant_entry -> constant_body diff --git a/lib/flags.ml b/lib/flags.ml index 8ec4a2351..13f540379 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -84,12 +84,6 @@ let unsafe_set = ref Stringset.empty let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set let is_unsafe s = Stringset.mem s !unsafe_set -(* Flags for the virtual machine *) - -let boxed_definitions = ref true -let set_boxed_definitions b = boxed_definitions := b -let boxed_definitions _ = !boxed_definitions - (* Flags for external tools *) let subst_command_placeholder s t = diff --git a/lib/flags.mli b/lib/flags.mli index 7c4668677..ecb4d6dd6 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -65,11 +65,6 @@ val print_hyps_limit : unit -> int option val add_unsafe : string -> unit val is_unsafe : string -> bool -(** Options for the virtual machine *) - -val set_boxed_definitions : bool -> unit -val boxed_definitions : unit -> bool - (** Options for external tools *) (** Returns string format for default browser to use from Coq or CoqIDE *) diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 5ae048d65..ba40f98c0 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -15,8 +15,6 @@ type locality = | Local | Global -type boxed_flag = bool - type theorem_kind = | Theorem | Lemma @@ -52,7 +50,7 @@ type assumption_object_kind = Definitional | Logical | Conjectural *) type assumption_kind = locality * assumption_object_kind -type definition_kind = locality * boxed_flag * definition_object_kind +type definition_kind = locality * definition_object_kind (* Kinds used in proofs *) @@ -84,12 +82,12 @@ let string_of_theorem_kind = function | Proposition -> "Proposition" | Corollary -> "Corollary" -let string_of_definition_kind (l,boxed,d) = - match (l,d) with +let string_of_definition_kind def = + match def with | Local, Coercion -> "Coercion Local" | Global, Coercion -> "Coercion" | Local, Definition -> "Let" - | Global, Definition -> if boxed then "Boxed Definition" else "Definition" + | Global, Definition -> "Definition" | Local, SubClass -> "Local SubClass" | Global, SubClass -> "SubClass" | Global, CanonicalStructure -> "Canonical Structure" diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index 6b03442f5..88ef763c9 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -15,8 +15,6 @@ type locality = | Local | Global -type boxed_flag = bool - type theorem_kind = | Theorem | Lemma @@ -52,7 +50,7 @@ type assumption_object_kind = Definitional | Logical | Conjectural *) type assumption_kind = locality * assumption_object_kind -type definition_kind = locality * boxed_flag * definition_object_kind +type definition_kind = locality * definition_object_kind (** Kinds used in proofs *) @@ -74,7 +72,7 @@ type logical_kind = val logical_kind_of_goal_kind : goal_object_kind -> logical_kind val string_of_theorem_kind : theorem_kind -> string val string_of_definition_kind : - locality * boxed_flag * definition_object_kind -> string + locality * definition_object_kind -> string (** About locality *) diff --git a/library/declare.ml b/library/declare.ml index a9c463020..fa95fe313 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -160,8 +160,7 @@ let hcons_constant_declaration = function DefinitionEntry { const_entry_body = hcons1_constr ce.const_entry_body; const_entry_type = Option.map hcons1_constr ce.const_entry_type; - const_entry_opaque = ce.const_entry_opaque; - const_entry_boxed = ce.const_entry_boxed } + const_entry_opaque = ce.const_entry_opaque } | cd -> cd let declare_constant_common id dhyps (cd,kind) = diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4abc2e5eb..f6943871c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -152,10 +152,6 @@ GEXTEND Gram | stre = assumptions_token; nl = inline; bl = assum_list -> test_plurial_form bl; VernacAssumption (stre, nl, bl) - | IDENT "Boxed";"Definition";id = identref; b = def_body -> - VernacDefinition ((Global,true,Definition), id, b, no_hook) - | IDENT "Unboxed";"Definition";id = identref; b = def_body -> - VernacDefinition ((Global,false,Definition), id, b, no_hook) | (f,d) = def_token; id = identref; b = def_body -> VernacDefinition (d, id, b, f) (* Gallina inductive declarations *) @@ -164,14 +160,10 @@ GEXTEND Gram let (k,f) = f in let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in VernacInductive (f,false,indl) - | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (recs,true) - | IDENT "Unboxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (recs,false) - | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (recs,Flags.boxed_definitions()) + | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint recs | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (corecs,false) + VernacCoFixpoint corecs | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ] @@ -201,13 +193,13 @@ GEXTEND Gram ; def_token: [ [ "Definition" -> - no_hook, (Global, Flags.boxed_definitions(), Definition) + no_hook, (Global, Definition) | IDENT "Let" -> - no_hook, (Local, Flags.boxed_definitions(), Definition) + no_hook, (Local, Definition) | IDENT "Example" -> - no_hook, (Global, Flags.boxed_definitions(), Example) + no_hook, (Global, Example) | IDENT "SubClass" -> - Class.add_subclass_hook, (use_locality_exp (), false, SubClass) ] ] + Class.add_subclass_hook, (use_locality_exp (), SubClass) ] ] ; assumption_token: [ [ "Hypothesis" -> (Local, Logical) @@ -510,16 +502,16 @@ GEXTEND Gram d = def_body -> let s = coerce_reference_to_id qid in VernacDefinition - ((Global,false,CanonicalStructure),(dummy_loc,s),d, + ((Global,CanonicalStructure),(dummy_loc,s),d, (fun _ -> Recordops.declare_canonical_structure)) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((use_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + VernacDefinition ((use_locality_exp (),Coercion),(dummy_loc,s),d,Class.add_coercion_hook) | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((enforce_locality_exp true,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + VernacDefinition ((enforce_locality_exp true,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (enforce_locality_exp true, f, s, t) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 0583403df..21281f6e4 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -607,7 +607,7 @@ let rec pr_vernac = function (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) - | VernacFixpoint (recs,b) -> + | VernacFixpoint recs -> let pr_onerec = function | ((loc,id),ro,bl,type_,def),ntn -> let annot = pr_guard_annot bl ro in @@ -616,19 +616,17 @@ let rec pr_vernac = function ++ pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++ prlist (pr_decl_notation pr_constr) ntn in - let start = if b then "Boxed Fixpoint" else "Fixpoint" in - hov 0 (str start ++ spc() ++ + hov 0 (str "Fixpoint" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs) - | VernacCoFixpoint (corecs,b) -> + | VernacCoFixpoint corecs -> let pr_onecorec (((loc,id),bl,c,def),ntn) = pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ spc() ++ pr_lconstr_expr c ++ pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++ prlist (pr_decl_notation pr_constr) ntn in - let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in - hov 0 (str start ++ spc() ++ + hov 0 (str "CoFixpoint" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs) | VernacScheme l -> hov 2 (str"Scheme" ++ spc() ++ diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 0cc5af99f..1d089409b 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 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 diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 3ab9d58d5..feff5d67c 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) = diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v index f05e00338..e2d8e67e6 100644 --- a/plugins/quote/Quote.v +++ b/plugins/quote/Quote.v @@ -26,7 +26,6 @@ Declare ML Module "quote_plugin". ***********************************************************************) Set Implicit Arguments. -Unset Boxed Definitions. Section variables_map. diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v index 9259d490f..fd5bcd935 100644 --- a/plugins/ring/LegacyArithRing.v +++ b/plugins/ring/LegacyArithRing.v @@ -15,7 +15,7 @@ Require Import Eqdep_dec. Open Local Scope nat_scope. -Unboxed Fixpoint nateq (n m:nat) {struct m} : bool := +Fixpoint nateq (n m:nat) {struct m} : bool := match n, m with | O, O => true | S n', S m' => nateq n' m' diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v index fa7709982..5dcd6d840 100644 --- a/plugins/ring/LegacyNArithRing.v +++ b/plugins/ring/LegacyNArithRing.v @@ -14,7 +14,7 @@ Require Export ZArith_base. Require Import NArith. Require Import Eqdep_dec. -Unboxed Definition Neq (n m:N) := +Definition Neq (n m:N) := match (n ?= m)%N with | Datatypes.Eq => true | _ => false diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v index 87b64c8d8..5845062dd 100644 --- a/plugins/ring/LegacyZArithRing.v +++ b/plugins/ring/LegacyZArithRing.v @@ -13,7 +13,7 @@ Require Export ZArith_base. Require Import Eqdep_dec. Require Import LegacyRing. -Unboxed Definition Zeq (x y:Z) := +Definition Zeq (x y:Z) := match (x ?= y)%Z with | Datatypes.Eq => true | _ => false diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v index e009f14ea..1763d70a6 100644 --- a/plugins/ring/Ring_abstract.v +++ b/plugins/ring/Ring_abstract.v @@ -10,8 +10,6 @@ Require Import LegacyRing_theory. Require Import Quote. Require Import Ring_normalize. -Unset Boxed Definitions. - Section abstract_semi_rings. Inductive aspolynomial : Type := diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v index 073cd2f63..e499f2220 100644 --- a/plugins/ring/Ring_normalize.v +++ b/plugins/ring/Ring_normalize.v @@ -10,7 +10,6 @@ Require Import LegacyRing_theory. Require Import Quote. Set Implicit Arguments. -Unset Boxed Definitions. Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m. Proof. diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v index d157bffce..41190e8d9 100644 --- a/plugins/ring/Setoid_ring_normalize.v +++ b/plugins/ring/Setoid_ring_normalize.v @@ -10,7 +10,6 @@ Require Import Setoid_ring_theory. Require Import Quote. Set Implicit Arguments. -Unset Boxed Definitions. Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m. Proof. diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 769869584..6c250ef4f 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -9,8 +9,6 @@ Require Export List. Require Export BinPos. -Unset Boxed Definitions. - Open Scope positive_scope. Ltac clean := try (simpl; congruence). diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index e80542831..f5d452f7e 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -10,7 +10,6 @@ Require Export List. Require Export Bintree. Require Import Bool. -Unset Boxed Definitions. Declare ML Module "rtauto_plugin". diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 9a79f2878..38c65cdd0 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -159,8 +159,7 @@ let decl_constant na c = mkConst(declare_constant (id_of_string na) (DefinitionEntry { const_entry_body = c; const_entry_type = None; - const_entry_opaque = true; - const_entry_boxed = true}, + const_entry_opaque = true }, IsProof Lemma)) (* Calling a global tactic *) diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index e614085e4..fbdaa8d3b 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -141,12 +141,12 @@ let subtac (loc, command) = (fun _ _ -> ()) | DefineBody (bl, _, c, tycon) -> ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon)) - | VernacFixpoint (l, b) -> + | VernacFixpoint l -> List.iter (fun ((lid, _, _, _, _), _) -> check_fresh lid; Dumpglob.dump_definition lid false "fix") l; let _ = trace (str "Building fixpoint") in - ignore(Subtac_command.build_recursive l b) + ignore(Subtac_command.build_recursive l) | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) -> if guard <> None then @@ -171,10 +171,10 @@ let subtac (loc, command) = error "Declare Instance not supported here."; ignore(Subtac_classes.new_instance ~global:glob sup is props pri) - | VernacCoFixpoint (l, b) -> + | VernacCoFixpoint l -> if Dumpglob.dump () then List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l; - ignore(Subtac_command.build_corecursive l b) + ignore(Subtac_command.build_corecursive l) (*| VernacEndProof e -> subtac_end_proof e*) diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index 0d5f7b86e..aae538389 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -176,4 +176,4 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p in let evm = Subtac_utils.evars_of_term !evars Evd.empty term in let obls, _, constr, typ = Eterm.eterm_obligations env id !evars evm 0 term termtype in - id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,false,Instance) ~hook obls + id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,Instance) ~hook obls diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 794143de4..9098922e3 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -215,7 +215,7 @@ let nf_evar_context isevars ctx = List.map (fun (n, b, t) -> (n, Option.map (Evarutil.nf_evar isevars) b, Evarutil.nf_evar isevars t)) ctx -let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = +let build_wellfounded (recname,n,bl,arityc,body) r measure notation = Coqlib.check_required_library ["Coq";"Program";"Wf"]; let sigma = Evd.empty in let isevars = ref (Evd.create_evar_defs sigma) in @@ -327,8 +327,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = let ce = { const_entry_body = Evarutil.nf_evar !isevars body; const_entry_type = Some ty; - const_entry_opaque = false; - const_entry_boxed = false} + const_entry_opaque = false } in let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in @@ -417,7 +416,7 @@ let out_def = function | Some def -> def | None -> error "Program Fixpoint needs defined bodies." -let interp_recursive fixkind l boxed = +let interp_recursive fixkind l = let env = Global.env() in let fixl, ntnl = List.split l in let kind = fixkind <> IsCoFixpoint in @@ -506,7 +505,7 @@ let out_n = function Some n -> n | None -> raise Not_found -let build_recursive l b = +let build_recursive l = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in match g, l with [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] -> @@ -514,24 +513,24 @@ let build_recursive l b = (match n with Some n -> mkIdentC (snd n) | None -> errorlabstrm "Subtac_command.build_recursive" (str "Recursive argument required for well-founded fixpoints")) - ntn false) + ntn) | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] -> ignore(build_wellfounded (id, n, bl, typ, out_def def) (Option.default (CRef lt_ref) r) - m ntn false) + m ntn) | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g -> let fixl = List.map (fun (((_,id),(n,ro),bl,typ,def),ntn) -> ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = n; Command.fix_body = def; Command.fix_type = typ},ntn)) l - in interp_recursive (IsFixpoint g) fixl b + in interp_recursive (IsFixpoint g) fixl | _, _ -> errorlabstrm "Subtac_command.build_recursive" (str "Well-founded fixpoints not allowed in mutually recursive blocks") -let build_corecursive l b = +let build_corecursive l = let fixl = List.map (fun (((_,id),bl,typ,def),ntn) -> ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = None; Command.fix_body = def; Command.fix_type = typ},ntn)) l in - interp_recursive IsCoFixpoint fixl b + interp_recursive IsCoFixpoint fixl diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli index 55991c8e8..72549a011 100644 --- a/plugins/subtac/subtac_command.mli +++ b/plugins/subtac/subtac_command.mli @@ -51,10 +51,10 @@ val build_wellfounded : Names.identifier * 'a * Topconstr.local_binder list * Topconstr.constr_expr * Topconstr.constr_expr -> Topconstr.constr_expr -> - Topconstr.constr_expr -> 'b -> 'c -> Subtac_obligations.progress + Topconstr.constr_expr -> 'b -> Subtac_obligations.progress val build_recursive : - (fixpoint_expr * decl_notation list) list -> bool -> unit + (fixpoint_expr * decl_notation list) list -> unit val build_corecursive : - (cofixpoint_expr * decl_notation list) list -> bool -> unit + (cofixpoint_expr * decl_notation list) list -> unit diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index d61ca2bc8..3d1e836a7 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -184,12 +184,11 @@ let declare_definition prg = my_print_constr (Global.env()) body ++ str " : " ++ my_print_constr (Global.env()) prg.prg_type); with _ -> ()); - let (local, boxed, kind) = prg.prg_kind in + let (local, kind) = prg.prg_kind in let ce = { const_entry_body = body; const_entry_type = Some typ; - const_entry_opaque = false; - const_entry_boxed = boxed} + const_entry_opaque = false } in (Command.get_declare_definition_hook ()) ce; match local with @@ -207,7 +206,7 @@ let declare_definition prg = | (Global|Local) -> let c = Declare.declare_constant - prg.prg_name (DefinitionEntry ce,IsDefinition (pi3 prg.prg_kind)) + prg.prg_name (DefinitionEntry ce,IsDefinition (snd prg.prg_kind)) in let gr = ConstRef c in if Impargs.is_implicit_args () || prg.prg_implicits <> [] then @@ -255,7 +254,7 @@ let declare_mutual_definition l = let fixkind = Option.get first.prg_fixkind in let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in - let (local,boxed,kind) = first.prg_kind in + let (local,kind) = first.prg_kind in let fixnames = first.prg_deps in let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in let indexes, fixdecls = @@ -269,7 +268,7 @@ let declare_mutual_definition l = None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l in (* Declare the recursive definitions *) - let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in + let kns = list_map4 (declare_fix kind) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter Metasyntax.add_notation_interpretation first.prg_notations; Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames; @@ -288,8 +287,7 @@ let declare_obligation prg obl body = let ce = { const_entry_body = body; const_entry_type = Some ty; - const_entry_opaque = opaque; - const_entry_boxed = false} + const_entry_opaque = opaque } in let constant = Declare.declare_constant obl.obl_name (DefinitionEntry ce,IsProof Property) @@ -557,7 +555,7 @@ let show_term n = my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ my_print_constr (Global.env ()) prg.prg_body) -let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic +let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls = Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in @@ -575,7 +573,7 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?ta | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res | _ -> res) -let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) +let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce) ?(hook=fun _ _ -> ()) notations fixkind = let deps = List.map (fun (n, b, t, imps, obls) -> n) l in let upd = List.fold_left diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index cafe45485..3e8c71482 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -265,11 +265,11 @@ let close_proof () = let id = get_current_proof_name () in let p = give_me_the_proof () in let proofs_and_types = Proof.return p in - let entries = List.map (fun (c,t) -> { Entries.const_entry_body = c ; - const_entry_type = Some t; - const_entry_opaque = true ; - const_entry_boxed = false } ) - proofs_and_types + let entries = List.map + (fun (c,t) -> { Entries.const_entry_body = c ; + const_entry_type = Some t; + const_entry_opaque = true }) + proofs_and_types in let { compute_guard=cg ; strength=str ; hook=hook } = Idmap.find id !proof_info diff --git a/scripts/coqc.ml b/scripts/coqc.ml index eb33850a7..57453ac4d 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -147,12 +147,10 @@ let parse_args () = | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem | ("-notactics"|"-debug"|"-nolib" - |"-debugVM"|"-alltransp"|"-VMno" |"-batch"|"-nois"|"-noglob"|"-no-glob" |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" - |"-dont-load-proofs"|"-load-proofs"|"-impredicative-set"|"-vm" - |"-unboxed-values"|"-unboxed-definitions"|"-draw-vm-instr" as o) :: rem -> + |"-dont-load-proofs"|"-load-proofs"|"-impredicative-set"|"-vm" as o) :: rem -> parse (cfiles,o::args) rem | ("-where") :: _ -> diff --git a/tactics/leminv.ml b/tactics/leminv.ml index c31980158..95814302d 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -236,8 +236,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op = (DefinitionEntry { const_entry_body = invProof; const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = true && (Flags.boxed_definitions())}, + const_entry_opaque = false }, IsProof Lemma) in () diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 188bc3dc5..a6a36672b 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1345,8 +1345,7 @@ let declare_projection n instance_id r = let cst = { const_entry_body = term; const_entry_type = Some typ; - const_entry_opaque = false; - const_entry_boxed = false } + const_entry_opaque = false } in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index fd902aa84..1dd5ce16c 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -13,7 +13,7 @@ Open Local Scope nat_scope. (** Factorial *) -Boxed Fixpoint fact (n:nat) : nat := +Fixpoint fact (n:nat) : nat := match n with | O => 1 | S n => S n * fact n diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 216ca35af..03487b6d6 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -26,7 +26,6 @@ Require Import Notations. Require Import Datatypes. Require Import Logic. -Unset Boxed Definitions. Open Scope nat_scope. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 81e2e06e4..686a0692c 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -7,7 +7,6 @@ (************************************************************************) Require Import BinPos. -Unset Boxed Definitions. (**********************************************************************) (** Binary natural numbers *) diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 97d935e4f..d2e6c70b9 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -13,8 +13,6 @@ Require Import Wf_nat. Require Export ZArith. Require Export DoubleType. -Unset Boxed Definitions. - (** * 31-bit integers *) (** This file contains basic definitions of a 31-bit integer diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 0ffce766c..64e32c560 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Unset Boxed Definitions. - Declare ML Module "z_syntax_plugin". (**********************************************************************) @@ -65,8 +63,6 @@ Fixpoint Psucc (x:positive) : positive := (** ** Addition *) -Set Boxed Definitions. - Fixpoint Pplus (x y:positive) : positive := match x, y with | p~1, q~1 => (Pplus_carry p q)~0 @@ -93,8 +89,6 @@ with Pplus_carry (x y:positive) : positive := | 1, 1 => 1~1 end. -Unset Boxed Definitions. - Infix "+" := Pplus : positive_scope. Definition Piter_op {A}(op:A->A->A) := diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index cbf6da197..e858d2148 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -105,7 +105,7 @@ Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real. (**********************************************************) (**********) -Boxed Fixpoint INR (n:nat) : R := +Fixpoint INR (n:nat) : R := match n with | O => 0 | S O => 1 diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 525eff688..1eee8d852 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -659,7 +659,7 @@ Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z). (** * Sum of n first naturals *) (*******************************) (*********) -Boxed Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) : nat := +Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) : nat := match n with | O => f 0%nat | S n' => (sum_nat_f_O f n' + f (S n'))%nat diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 0687bfbc2..d16e7f2c7 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -147,7 +147,7 @@ Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist := | existT a b => a end. -Boxed Fixpoint Int_SF (l k:Rlist) : R := +Fixpoint Int_SF (l k:Rlist) : R := match l with | nil => 0 | cons a l' => diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 76d66ca06..12258d6b5 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -15,7 +15,7 @@ Require Import Binomial. Open Local Scope R_scope. (** TT Ak; 0<=k<=N *) -Boxed Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R := +Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R := match N with | O => f O | S p => prod_f_R0 f p * f (S p) diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 5f8b5d9da..479d381d4 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -25,7 +25,7 @@ Section sequence. Variable Un : nat -> R. (*********) - Boxed Fixpoint Rmax_N (N:nat) : R := + Fixpoint Rmax_N (N:nat) : R := match N with | O => Un 0 | S n => Rmax (Un (S n)) (Rmax_N n) diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 2fdf1ffea..8c46f355f 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -13,7 +13,7 @@ Require Import SeqSeries. Require Import Ranalysis1. Open Local Scope R_scope. -Boxed Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R := +Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R := match N with | O => x | S n => diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index a5fdf855a..ad3781832 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -15,8 +15,6 @@ Require Export BinPos Pnat. Require Import BinNat Plus Mult. -Unset Boxed Definitions. - Inductive Z : Set := | Z0 : Z | Zpos : positive -> Z @@ -1002,13 +1000,13 @@ Qed. (**********************************************************************) (** * Minimum and maximum *) -Unboxed Definition Zmax (n m:Z) := +Definition Zmax (n m:Z) := match n ?= m with | Eq | Gt => n | Lt => m end. -Unboxed Definition Zmin (n m:Z) := +Definition Zmin (n m:Z) := match n ?= m with | Eq | Lt => n | Gt => m diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index 4f4a6078c..45fcc17be 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -13,7 +13,6 @@ Require Import Zcompare. Require Import ZArith_dec. Require Import Sumbool. -Unset Boxed Definitions. Open Local Scope Z_scope. (** * Boolean operations from decidability of order *) diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 53fee9875..605196d6f 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -29,7 +29,7 @@ let build_table l = let is_keyword = build_table - [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; + [ "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; "Hypotheses"; @@ -41,8 +41,7 @@ let is_keyword = "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; "Notation"; "Reserved Notation"; "Tactic Notation"; - "Delimit"; "Bind"; "Open"; "Scope"; - "Boxed"; "Unboxed"; "Inline"; + "Delimit"; "Bind"; "Open"; "Scope"; "Inline"; "Implicit Arguments"; "Add"; "Strict"; "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation"; "subgoal"; diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 4c2353fc8..242a8e52b 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -179,8 +179,9 @@ let declare_record_instance gr ctx params = let ident = make_instance_ident gr in let def = it_mkLambda_or_LetIn (applistc (constr_of_global gr) params) ctx in let def = deep_refresh_universes def in - let ce = { const_entry_body=def; const_entry_type=None; - const_entry_opaque=false; const_entry_boxed=false } in + let ce = { const_entry_body=def; + const_entry_type=None; + const_entry_opaque=false } in let cst = Declare.declare_constant ident (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in new_instance_message ident (Typeops.type_of_constant (Global.env()) cst) def @@ -193,8 +194,9 @@ let declare_class_instance gr ctx params = let def = deep_refresh_universes def in let typ = deep_refresh_universes typ in let ce = Entries.DefinitionEntry - { const_entry_type=Some typ; const_entry_body=def; - const_entry_opaque=false; const_entry_boxed=false } in + { const_entry_type=Some typ; + const_entry_body=def; + const_entry_opaque=false } in try let cst = Declare.declare_constant ident (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in diff --git a/toplevel/class.ml b/toplevel/class.ml index 7f5dacaae..76d8750cb 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -218,8 +218,7 @@ let build_id_coercion idf_opt source = DefinitionEntry { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f); const_entry_type = Some typ_f; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions()} in + const_entry_opaque = false } in let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in ConstRef kn diff --git a/toplevel/classes.ml b/toplevel/classes.ml index f5a450a5c..f11bdb4a8 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -108,8 +108,7 @@ let declare_instance_constant k pri global imps ?hook id term termtype = let entry = { const_entry_body = term; const_entry_type = Some termtype; - const_entry_opaque = false; - const_entry_boxed = false } + const_entry_opaque = false } in DefinitionEntry entry, kind in let kn = Declare.declare_constant id cdecl in diff --git a/toplevel/command.ml b/toplevel/command.ml index 93b05290f..c180785d5 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -64,7 +64,7 @@ let red_constant_entry n ce = function { ce with const_entry_body = under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body } -let interp_definition boxed bl red_option c ctypopt = +let interp_definition bl red_option c ctypopt = let env = Global.env() in let evdref = ref Evd.empty in let (env_bl, ctx), imps1 = interp_context_evars evdref env bl in @@ -77,8 +77,7 @@ let interp_definition boxed bl red_option c ctypopt = imps1@imps2, { const_entry_body = body; const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = boxed } + const_entry_opaque = false } | Some ctyp -> let ty, impls = interp_type_evars_impls ~evdref ~fail_evar:false env_bl ctyp in let c, imps2 = interp_casted_constr_evars_impls ~evdref ~fail_evar:false env_bl c ty in @@ -89,8 +88,7 @@ let interp_definition boxed bl red_option c ctypopt = imps1@imps2, { const_entry_body = body; const_entry_type = Some typ; - const_entry_opaque = false; - const_entry_boxed = boxed } + const_entry_opaque = false } in red_constant_entry (rel_context_length ctx) ce red_option, imps @@ -469,13 +467,12 @@ let interp_fix_body evdref env_rec impls (_,ctx) fix ccl = let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx -let declare_fix boxed kind f def t imps = +let declare_fix kind f def t imps = let ce = { const_entry_body = def; const_entry_type = Some t; - const_entry_opaque = false; - const_entry_boxed = boxed - } in + const_entry_opaque = false } + in let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in let gr = ConstRef kn in Autoinstance.search_declaration (ConstRef kn); @@ -545,7 +542,7 @@ let interp_recursive isfix fixl notations = let interp_fixpoint = interp_recursive true let interp_cofixpoint = interp_recursive false -let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = +let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = if List.mem None fixdefs then (* Some bodies to define by proof *) let thms = @@ -563,14 +560,14 @@ let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = let fiximps = List.map (fun (n,r,p) -> r) fiximps in let fixdecls = list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in - ignore (list_map4 (declare_fix boxed Fixpoint) fixnames fixdecls fixtypes fiximps); + ignore (list_map4 (declare_fix Fixpoint) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) fixpoint_message (Some indexes) fixnames; end; (* Declare notations *) List.iter Metasyntax.add_notation_interpretation ntns -let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns = +let declare_cofixpoint ((fixnames,fixdefs,fixtypes),fiximps) ntns = if List.mem None fixdefs then (* Some bodies to define by proof *) let thms = @@ -586,7 +583,7 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns = let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in - ignore (list_map4 (declare_fix boxed CoFixpoint) fixnames fixdecls fixtypes fiximps); + ignore (list_map4 (declare_fix CoFixpoint) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames end; @@ -612,13 +609,13 @@ let extract_cofixpoint_components l = {fix_name = id; fix_annot = None; fix_binders = bl; fix_body = def; fix_type = typ}) fixl, List.flatten ntnl -let do_fixpoint l b = +let do_fixpoint l = let fixl,ntns = extract_fixpoint_components true l in let fix = interp_fixpoint fixl ntns in let possible_indexes = List.map compute_possible_guardness_evidences (snd fix) in - declare_fixpoint b fix possible_indexes ntns + declare_fixpoint fix possible_indexes ntns -let do_cofixpoint l b = +let do_cofixpoint l = let fixl,ntns = extract_cofixpoint_components l in - declare_cofixpoint b (interp_cofixpoint fixl ntns) ntns + declare_cofixpoint (interp_cofixpoint fixl ntns) ntns diff --git a/toplevel/command.mli b/toplevel/command.mli index 47387b8c2..163f68fd0 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -31,7 +31,7 @@ val set_declare_assumptions_hook : (types -> unit) -> unit (** {6 Definitions/Let} *) val interp_definition : - boxed_flag -> local_binder list -> red_expr option -> constr_expr -> + local_binder list -> red_expr option -> constr_expr -> constr_expr option -> definition_entry * manual_implicits val declare_definition : identifier -> locality * definition_object_kind -> @@ -127,26 +127,24 @@ val interp_cofixpoint : (** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : - bool -> recursive_preentry * (name list * manual_implicits * int option) list -> lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : - bool -> recursive_preentry * (name list * manual_implicits * int option) list -> decl_notation list -> unit (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint : - (fixpoint_expr * decl_notation list) list -> bool -> unit + (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint : - (cofixpoint_expr * decl_notation list) list -> bool -> unit + (cofixpoint_expr * decl_notation list) list -> unit (** Utils *) val check_mutuality : Environ.env -> bool -> (identifier * types) list -> unit -val declare_fix : bool -> definition_object_kind -> identifier -> +val declare_fix : definition_object_kind -> identifier -> constr -> types -> Impargs.manual_explicitation list -> global_reference diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 6d98d3dd0..b85c00714 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -128,12 +128,10 @@ let set_compat_version = function (*s options for the virtual machine *) let boxed_val = ref false -let boxed_def = ref false let use_vm = ref false let set_vm_opt () = Vm.set_transp_values (not !boxed_val); - Flags.set_boxed_definitions !boxed_def; Vconv.set_use_vm !use_vm (*s Parsing of the command line. diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index daa93a7e6..51dc1dc30 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -115,8 +115,7 @@ let define internal id c = (DefinitionEntry { const_entry_body = c; const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() }, + const_entry_opaque = false }, Decl_kinds.IsDefinition Scheme) in (match internal with | KernelSilent -> () diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 8d8997a2b..f7ff2013b 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -105,8 +105,7 @@ let define id internal c t = (DefinitionEntry { const_entry_body = c; const_entry_type = t; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() }, + const_entry_opaque = false }, Decl_kinds.IsDefinition Scheme) in definition_message id; kn diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 0d7a3b2f9..847278b07 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -216,8 +216,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) = let const = { const_entry_body = body_i; const_entry_type = Some t_i; - const_entry_opaque = opaq; - const_entry_boxed = false (* copy of what cook_proof does *)} in + const_entry_opaque = opaq } in let kn = declare_constant id (DefinitionEntry const, k) in (Global,ConstRef kn,imps) diff --git a/toplevel/record.ml b/toplevel/record.ml index ea11ca487..27b6ffabe 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -201,8 +201,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls let cie = { const_entry_body = proj; const_entry_type = Some projtyp; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() } in + const_entry_opaque = false } in let k = (DefinitionEntry cie,IsDefinition kind) in let kn = declare_constant ~internal:KernelSilent fid k in Flags.if_verbose message (string_of_id fid ^" is defined"); @@ -311,8 +310,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls let class_entry = { const_entry_body = class_body; const_entry_type = class_type; - const_entry_opaque = false; - const_entry_boxed = false } + const_entry_opaque = false } in let cst = Declare.declare_constant (snd id) (DefinitionEntry class_entry, IsDefinition Definition) @@ -323,8 +321,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls let proj_entry = { const_entry_body = proj_body; const_entry_type = Some proj_type; - const_entry_opaque = false; - const_entry_boxed = false } + const_entry_opaque = false } in let proj_cst = Declare.declare_constant proj_name (DefinitionEntry proj_entry, IsDefinition Definition) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 16817143d..a18340e90 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -328,7 +328,7 @@ let start_proof_and_print k l hook = print_subgoals (); if !pcoq <> None then (Option.get !pcoq).start_proof () -let vernac_definition (local,boxed,k) (loc,id as lid) def hook = +let vernac_definition (local,k) (loc,id as lid) def hook = if local = Local then Dumpglob.dump_definition lid true "var" else Dumpglob.dump_definition lid false "def"; (match def with @@ -342,7 +342,7 @@ let vernac_definition (local,boxed,k) (loc,id as lid) def hook = | Some r -> let (evc,env)= get_current_context () in Some (interp_redexp env evc r) in - let ce,imps = interp_definition boxed bl red_option c typ_opt in + let ce,imps = interp_definition bl red_option c typ_opt in declare_definition id (local,k) ce imps hook) let vernac_start_proof kind l lettop hook = @@ -433,15 +433,15 @@ let vernac_inductive finite infer indl = let indl = List.map unpack indl in do_mutual_inductive indl (recursivity_flag_of_kind finite) -let vernac_fixpoint l b = +let vernac_fixpoint l = if Dumpglob.dump () then List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - do_fixpoint l b + do_fixpoint l -let vernac_cofixpoint l b = +let vernac_cofixpoint l = if Dumpglob.dump () then List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - do_cofixpoint l b + do_cofixpoint l let vernac_scheme = Indschemes.do_scheme @@ -943,14 +943,6 @@ let _ = let _ = declare_bool_option { optsync = true; - optname = "use of boxed definitions"; - optkey = ["Boxed";"Definitions"]; - optread = Flags.boxed_definitions; - optwrite = (fun b -> Flags.set_boxed_definitions b) } - -let _ = - declare_bool_option - { optsync = true; optname = "use of boxed values"; optkey = ["Boxed";"Values"]; optread = (fun _ -> not (Vm.transp_values ())); @@ -1338,8 +1330,8 @@ let interp c = match c with | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl | VernacInductive (finite,infer,l) -> vernac_inductive finite infer l - | VernacFixpoint (l,b) -> vernac_fixpoint l b - | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b + | VernacFixpoint l -> vernac_fixpoint l + | VernacCoFixpoint l -> vernac_cofixpoint l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 72c9b1fe8..80191b8fd 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -228,8 +228,8 @@ type vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list - | VernacFixpoint of (fixpoint_expr * decl_notation list) list * bool - | VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list * bool + | VernacFixpoint of (fixpoint_expr * decl_notation list) list + | VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list |