diff options
| author | Pierre-Marie Pédrot | 2016-06-17 20:26:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-18 18:54:43 +0200 |
| commit | ecb032467557631ea60324c6afa55c91c133e40d (patch) | |
| tree | 831803ca1db0e73ec3cea91c52f5f2e288d12341 /toplevel/command.ml | |
| parent | 53ced0735f7e24735d78a02fc74588b8d9186eab (diff) | |
Reuse the typing_flags datatype for inductives.
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 643b066609..5041d78a33 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 *) |