aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/functional_principles_types.ml4
-rw-r--r--plugins/funind/indfun.ml5
-rw-r--r--plugins/funind/recdef.ml3
-rw-r--r--plugins/quote/Quote.v1
-rw-r--r--plugins/ring/LegacyArithRing.v2
-rw-r--r--plugins/ring/LegacyNArithRing.v2
-rw-r--r--plugins/ring/LegacyZArithRing.v2
-rw-r--r--plugins/ring/Ring_abstract.v2
-rw-r--r--plugins/ring/Ring_normalize.v1
-rw-r--r--plugins/ring/Setoid_ring_normalize.v1
-rw-r--r--plugins/rtauto/Bintree.v2
-rw-r--r--plugins/rtauto/Rtauto.v1
-rw-r--r--plugins/setoid_ring/newring.ml43
-rw-r--r--plugins/subtac/subtac.ml8
-rw-r--r--plugins/subtac/subtac_classes.ml2
-rw-r--r--plugins/subtac/subtac_command.ml19
-rw-r--r--plugins/subtac/subtac_command.mli6
-rw-r--r--plugins/subtac/subtac_obligations.ml18
18 files changed, 33 insertions, 49 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) =
diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v
index f05e003387..e2d8e67e6b 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 9259d490fb..fd5bcd9355 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 fa77099826..5dcd6d840d 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 87b64c8d8f..5845062dd2 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 e009f14eaa..1763d70a62 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 073cd2f63c..e499f22201 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 d157bffce9..41190e8d9a 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 769869584d..6c250ef4f9 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 e805428313..f5d452f7e6 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 9a79f28783..38c65cdd09 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 e614085e48..fbdaa8d3b1 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 0d5f7b86e0..aae5383892 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 794143de49..9098922e31 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 55991c8e88..72549a011e 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 d61ca2bc8b..3d1e836a78 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:32:04 +0000