aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/declarations.mli5
-rw-r--r--kernel/declareops.ml3
-rw-r--r--kernel/entries.mli2
-rw-r--r--kernel/environ.ml3
-rw-r--r--kernel/environ.mli1
-rw-r--r--kernel/indtypes.ml9
-rw-r--r--library/declare.ml2
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/merge.ml2
-rw-r--r--toplevel/assumptions.ml2
-rw-r--r--toplevel/command.ml13
-rw-r--r--toplevel/command.mli2
-rw-r--r--toplevel/discharge.ml1
-rw-r--r--toplevel/indschemes.ml2
-rw-r--r--toplevel/record.ml18
-rw-r--r--toplevel/record.mli2
-rw-r--r--toplevel/vernacentries.ml19
17 files changed, 38 insertions, 50 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index ef4d398c1..f89773fcc 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -190,11 +190,8 @@ type mutual_inductive_body = {
mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
-
- mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker. *)
-
- mind_unsafe_universes : bool; (** generated with the type-in-type flag *)
+ mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *)
}
(** {6 Module declarations } *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 5caf052ac..211e5e062 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -261,8 +261,7 @@ let subst_mind_body sub mib =
mind_polymorphic = mib.mind_polymorphic;
mind_universes = mib.mind_universes;
mind_private = mib.mind_private;
- mind_checked_positive = mib.mind_checked_positive;
- mind_unsafe_universes = mib.mind_unsafe_universes;
+ mind_typing_flags = mib.mind_typing_flags;
}
let inductive_instance mib =
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 8b29e3abd..df2c4653f 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -52,8 +52,6 @@ type mutual_inductive_entry = {
mind_entry_polymorphic : bool;
mind_entry_universes : Univ.universe_context;
mind_entry_private : bool option;
- mind_entry_check_positivity : bool;
- (** [false] if positivity is to be assumed. *)
}
(** {6 Constants (Definition/Axiom) } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 65aaa3f7b..9fb3bf79f 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -53,6 +53,7 @@ let is_impredicative_set env =
| _ -> false
let type_in_type env = not (typing_flags env).check_universes
+let deactivated_guard env = not (typing_flags env).check_guarded
let universes env = env.env_stratification.env_universes
let named_context env = env.env_named_context
@@ -362,7 +363,7 @@ let polymorphic_pind (ind,u) env =
else polymorphic_ind ind env
let type_in_type_ind (mind,i) env =
- (lookup_mind mind env).mind_unsafe_universes
+ not (lookup_mind mind env).mind_typing_flags.check_universes
let template_polymorphic_ind (mind,i) env =
match (lookup_mind mind env).mind_packets.(i).mind_arity with
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 0edcb34de..b5e576435 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -53,6 +53,7 @@ val engagement : env -> engagement
val typing_flags : env -> typing_flags
val is_impredicative_set : env -> bool
val type_in_type : env -> bool
+val deactivated_guard : env -> bool
(** is the local context empty *)
val empty_context : env -> bool
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 34771034c..b6942e133 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -816,7 +816,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
Array.of_list (List.rev kns),
Array.of_list (List.rev pbs)
-let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs is_checked =
+let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs =
let ntypes = Array.length inds in
(* Compute the set of used section variables *)
let hyps = used_section_variables env inds in
@@ -922,8 +922,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
mind_polymorphic = p;
mind_universes = ctx;
mind_private = prv;
- mind_checked_positive = is_checked;
- mind_unsafe_universes = type_in_type env;
+ mind_typing_flags = Environ.typing_flags env;
}
(************************************************************************)
@@ -932,11 +931,11 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
let check_inductive env kn mie =
(* First type-check the inductive definition *)
let (env_ar, env_ar_par, paramsctxt, inds) = typecheck_inductive env mie in
- let chkpos = mie.mind_entry_check_positivity in
(* Then check positivity conditions *)
+ let chkpos = (Environ.typing_flags env).check_guarded in
let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in
(* Build the inductive packets *)
build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
mie.mind_entry_universes
env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite
- inds nmr recargs chkpos
+ inds nmr recargs
diff --git a/library/declare.ml b/library/declare.ml
index 4e9e68dff..f809e9742 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -354,7 +354,7 @@ let dummy_inductive_entry (_,m) = ([],{
mind_entry_polymorphic = false;
mind_entry_universes = Univ.UContext.empty;
mind_entry_private = None;
- mind_entry_check_positivity = true; })
+})
type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index f69c4d821..c424fe122 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1432,7 +1432,7 @@ let do_build_inductive
(* in *)
let _time2 = System.get_time () in
try
- with_full_print (Flags.silently (Command.do_mutual_inductive true rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite
+ with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite
with
| UserError(s,msg) as e ->
let _time3 = System.get_time () in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index a78eb1af7..99a165044 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -887,7 +887,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
(* Declare inductive *)
let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
- let mie,pl,impls = Command.interp_mutual_inductive true indl []
+ let mie,pl,impls = Command.interp_mutual_inductive indl []
false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
(* Declare the mutual inductive block with its associated schemes *)
ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls)
diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index 921c4a1d8..fb32ecac3 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -307,7 +307,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
accu
| IndRef (m,_) | ConstructRef ((m,_),_) ->
let mind = Global.lookup_mind m in
- if mind.mind_checked_positive then
+ if mind.mind_typing_flags.check_guarded then
accu
else
let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 643b06660..5041d78a3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -549,7 +549,7 @@ let check_param = function
| LocalRawAssum (nas, Default _, _) -> List.iter check_named nas
| LocalRawAssum (nas, Generalized _, _) -> ()
-let interp_mutual_inductive chk (paramsl,indl) notations poly prv finite =
+let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
check_all_names_different indl;
List.iter check_param paramsl;
let env0 = Global.env() in
@@ -631,7 +631,7 @@ let interp_mutual_inductive chk (paramsl,indl) notations poly prv finite =
mind_entry_polymorphic = poly;
mind_entry_private = if prv then Some false else None;
mind_entry_universes = uctx;
- mind_entry_check_positivity = chk; },
+ },
pl, impls
(* Very syntactical equality *)
@@ -716,19 +716,18 @@ type one_inductive_impls =
Impargs.manual_explicitation list (* for inds *)*
Impargs.manual_explicitation list list (* for constrs *)
-let do_mutual_inductive chk indl poly prv finite =
+let do_mutual_inductive indl poly prv finite =
let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
(* Interpret the types *)
- let mie,pl,impls = interp_mutual_inductive chk indl ntns poly prv finite in
+ let mie,pl,impls = interp_mutual_inductive indl ntns poly prv finite in
(* Declare the mutual inductive block with its associated schemes *)
ignore (declare_mutual_inductive_with_eliminations mie pl impls);
(* Declare the possible notations of inductive types *)
List.iter Metasyntax.add_notation_interpretation ntns;
(* Declare the coercions *)
List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes;
- (* If [chk] is [false] (i.e. positivity is assumed) declares itself
- as unsafe. *)
- if not chk then Feedback.feedback Feedback.AddedAxiom else ()
+ (* If positivity is assumed declares itself as unsafe. *)
+ if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else ()
(* 3c| Fixpoints and co-fixpoints *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index a5132cc66..d35372429 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -91,7 +91,6 @@ type one_inductive_impls =
Impargs.manual_implicits list (** for constrs *)
val interp_mutual_inductive :
- bool -> (* if [false], then positivity is assumed *)
structured_inductive_expr -> decl_notation list -> polymorphic ->
private_flag -> Decl_kinds.recursivity_kind ->
mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
@@ -106,7 +105,6 @@ val declare_mutual_inductive_with_eliminations :
(** Entry points for the vernacular commands Inductive and CoInductive *)
val do_mutual_inductive :
- bool -> (* if [false], then positivity is assumed *)
(one_inductive_expr * decl_notation list) list -> polymorphic ->
private_flag -> Decl_kinds.recursivity_kind -> unit
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 74361eb1c..fcb260f51 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -117,5 +117,4 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
mind_entry_polymorphic = mib.mind_polymorphic;
mind_entry_private = mib.mind_private;
mind_entry_universes = univs;
- mind_entry_check_positivity = mib.mind_checked_positive;
}
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index a43758e3c..a48bbf89d 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -497,7 +497,7 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
let declare_default_schemes kn =
let mib = Global.lookup_mind kn in
let n = Array.length mib.mind_packets in
- if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) && mib.mind_checked_positive then
+ if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) && mib.mind_typing_flags.check_guarded then
declare_induction_schemes kn;
if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
if is_eq_flag() then try_declare_beq_scheme kn;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 214d44d83..c9b46983e 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -361,7 +361,7 @@ let structure_signature ctx =
open Typeclasses
-let declare_structure chk finite poly ctx id idbuild paramimpls params arity template
+let declare_structure finite poly ctx id idbuild paramimpls params arity template
fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
let nparams = List.length params and nfields = List.length fields in
let args = Context.Rel.to_extended_list nfields params in
@@ -387,7 +387,8 @@ let declare_structure chk finite poly ctx id idbuild paramimpls params arity tem
mind_entry_polymorphic = poly;
mind_entry_private = None;
mind_entry_universes = ctx;
- mind_entry_check_positivity = chk; } in
+ }
+ in
let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let cstr = (rsp,1) in
@@ -406,7 +407,7 @@ let implicits_of_context ctx =
in ExplByPos (i, explname), (true, true, true))
1 (List.rev (Anonymous :: (List.map get_name ctx)))
-let declare_class chk finite def poly ctx id idbuild paramimpls params arity
+let declare_class finite def poly ctx id idbuild paramimpls params arity
template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
let fieldimpls =
(* Make the class implicit in the projections, and the params if applicable. *)
@@ -449,7 +450,7 @@ let declare_class chk finite def poly ctx id idbuild paramimpls params arity
in
cref, [Name proj_name, sub, Some proj_cst]
| _ ->
- let ind = declare_structure chk BiFinite poly ctx (snd id) idbuild paramimpls
+ let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
params arity template fieldimpls fields
~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
in
@@ -528,9 +529,8 @@ open Vernacexpr
(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
list telling if the corresponding fields must me declared as coercions
- or subinstances. When [chk] is false positivity is
- assumed. *)
-let definition_structure chk (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
+ or subinstances. *)
+let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
let cfs,notations = List.split cfs in
let cfs,priorities = List.split cfs in
let coers,fs = List.split cfs in
@@ -551,14 +551,14 @@ let definition_structure chk (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
let sign = structure_signature (fields@params) in
let gr = match kind with
| Class def ->
- let gr = declare_class chk finite def poly ctx (loc,idstruc) idbuild
+ let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
implpars params arity template implfs fields is_coe coers priorities sign in
gr
| _ ->
let implfs = List.map
(fun impls -> implpars @ Impargs.lift_implicits
(succ (List.length params)) impls) implfs in
- let ind = declare_structure chk finite poly ctx idstruc
+ let ind = declare_structure finite poly ctx idstruc
idbuild implpars params arity template implfs
fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
IndRef ind
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 525326237..b09425563 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -25,7 +25,6 @@ val declare_projections :
(Name.t * bool) list * constant option list
val declare_structure :
- bool -> (** check positivity? *)
Decl_kinds.recursivity_kind ->
bool (** polymorphic?*) -> Univ.universe_context ->
Id.t -> Id.t ->
@@ -39,7 +38,6 @@ val declare_structure :
inductive
val definition_structure :
- bool -> (** check positivity? *)
inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * plident with_coercion * local_binder list *
(local_decl_expr with_instance with_priority with_notation) list *
Id.t * constr_expr option -> global_reference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 29d6d7acd..82fe9751e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -519,7 +519,7 @@ let vernac_assumption locality poly (local, kind) l nl =
let status = do_assumptions kind nl l in
if not status then Feedback.feedback Feedback.AddedAxiom
-let vernac_record chk k poly finite struc binders sort nameopt cfs =
+let vernac_record k poly finite struc binders sort nameopt cfs =
let const = match nameopt with
| None -> add_prefix "Build_" (snd (fst (snd struc)))
| Some (_,id as lid) ->
@@ -530,14 +530,13 @@ let vernac_record chk k poly finite struc binders sort nameopt cfs =
match x with
| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
| _ -> ()) cfs);
- ignore(Record.definition_structure chk (k,poly,finite,struc,binders,cfs,const,sort))
+ ignore(Record.definition_structure (k,poly,finite,struc,binders,cfs,const,sort))
-(** When [chk] is false, positivity is assumed. When [poly] is true
- the type is declared polymorphic. When [lo] is true, then the type
- is declared private (as per the [Private] keyword). [finite]
+(** When [poly] is true the type is declared polymorphic. When [lo] is true,
+ then the type is declared private (as per the [Private] keyword). [finite]
indicates whether the type is inductive, co-inductive or
neither. *)
-let vernac_inductive chk poly lo finite indl =
+let vernac_inductive poly lo finite indl =
if Dumpglob.dump () then
List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
match cstrs with
@@ -553,14 +552,14 @@ let vernac_inductive chk poly lo finite indl =
| [ (_ , _ , _ ,Variant, RecordDecl _),_ ] ->
Errors.error "The Variant keyword cannot be used to define a record type. Use Record instead."
| [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
- vernac_record chk (match b with Class true -> Class false | _ -> b)
+ vernac_record (match b with Class true -> Class false | _ -> b)
poly finite id bl c oc fs
| [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
let f =
let (coe, ((loc, id), ce)) = l in
let coe' = if coe then Some true else None in
(((coe', AssumExpr ((loc, Name id), ce)), None), [])
- in vernac_record chk (Class true) poly finite id bl c None [f]
+ in vernac_record (Class true) poly finite id bl c None [f]
| [ ( id , bl , c , Class true, _), _ ] ->
Errors.error "Definitional classes must have a single method"
| [ ( id , bl , c , Class false, Constructors _), _ ] ->
@@ -574,7 +573,7 @@ let vernac_inductive chk poly lo finite indl =
| _ -> Errors.error "Cannot handle mutually (co)inductive records."
in
let indl = List.map unpack indl in
- do_mutual_inductive chk indl poly lo finite
+ do_mutual_inductive indl poly lo finite
let vernac_fixpoint locality poly local l =
let local = enforce_locality_exp locality local in
@@ -1767,7 +1766,7 @@ let interp ?proof ~loc locality poly c =
| VernacEndProof e -> vernac_end_proof ?proof e
| VernacExactProof c -> vernac_exact_proof c
| VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
- | VernacInductive (priv,finite,l) -> vernac_inductive true poly priv finite l
+ | VernacInductive (priv,finite,l) -> vernac_inductive poly priv finite l
| VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l
| VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
| VernacScheme l -> vernac_scheme l
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 22:46:55 +0000