diff options
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 41 |
1 files changed, 20 insertions, 21 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 348e76da62..9bbfb8eec6 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -24,7 +24,7 @@ open Constrexpr_ops open Constrintern open Impargs open Reductionops -open Indtypes +open Type_errors open Pretyping open Indschemes open Context.Rel.Declaration @@ -35,7 +35,7 @@ module RelDecl = Context.Rel.Declaration (* 3b| Mutual inductive definitions *) let warn_auto_template = - CWarnings.create ~name:"auto-template" ~category:"vernacular" + CWarnings.create ~name:"auto-template" ~category:"vernacular" ~default:CWarnings.Disabled (fun id -> Pp.(strbrk "Automatically declaring " ++ Id.print id ++ strbrk " as template polymorphic. Use attributes or " ++ @@ -83,10 +83,9 @@ type structured_one_inductive_expr = { type structured_inductive_expr = local_binder_expr list * structured_one_inductive_expr list -let minductive_message warn = function +let minductive_message = function | [] -> user_err Pp.(str "No inductive definition.") - | [x] -> (Id.print x ++ str " is defined" ++ - if warn then str " as a non-primitive record" else mt()) + | [x] -> (Id.print x ++ str " is defined") | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ spc () ++ str "are defined") @@ -163,7 +162,7 @@ let interp_cstrs env sigma impls mldata arity ind = let sigma, (ctyps'', cimpls) = on_snd List.split @@ List.fold_left_map (fun sigma l -> - interp_type_evars_impls env sigma ~impls l) sigma ctyps' in + interp_type_evars_impls ~program_mode:false env sigma ~impls l) sigma ctyps' in sigma, (cnames, ctyps'', cimpls) let sign_level env evd sign = @@ -304,7 +303,7 @@ let inductive_levels env evd poly arities inds = let evd = if Sorts.is_set du then if not (Evd.check_leq evd cu Univ.type0_univ) then - raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType) + raise (InductiveError LargeNonPropInductiveNotInType) else evd else evd (* Evd.set_leq_sort env evd (Type cu) du *) @@ -359,9 +358,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not then user_err (str "Inductives with uniform parameters may not have attached notations."); let sigma, udecl = interp_univ_decl_opt env0 udecl in let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) = - interp_context_evars env0 sigma uparamsl in + interp_context_evars ~program_mode:false env0 sigma uparamsl in let sigma, (impls, ((env_params, ctx_params), userimpls)) = - interp_context_evars ~impl_env:uimpls env_uparams sigma paramsl + interp_context_evars ~program_mode:false ~impl_env:uimpls env_uparams sigma paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in @@ -458,15 +457,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not indimpls, List.map (fun impls -> userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in - let univs = - match uctx with - | Polymorphic_const_entry (nas, uctx) -> - if cum then - Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context uctx) - else Polymorphic_ind_entry (nas, uctx) - | Monomorphic_const_entry uctx -> - Monomorphic_ind_entry uctx - in + let variance = if poly && cum then Some (InferCumulativity.dummy_variance uctx) else None in (* Build the mutual inductive entry *) let mind_ent = { mind_entry_params = ctx_params; @@ -474,7 +465,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not mind_entry_finite = finite; mind_entry_inds = entries; mind_entry_private = if prv then Some false else None; - mind_entry_universes = univs; + mind_entry_universes = uctx; + mind_entry_variance = variance; } in (if poly && cum then @@ -531,6 +523,12 @@ let is_recursive mie = List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc | _ -> false +let warn_non_primitive_record = + CWarnings.create ~name:"non-primitive-record" ~category:"record" + (fun indsp -> + (hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (IndRef indsp) ++ + strbrk" could not be defined as a primitive record"))) + let declare_mutual_inductive_with_eliminations mie pl impls = (* spiwack: raises an error if the structure is supposed to be non-recursive, but isn't *) @@ -545,6 +543,8 @@ let declare_mutual_inductive_with_eliminations mie pl impls = let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in let (_, kn), prim = declare_mind mie in let mind = Global.mind_of_delta_kn kn in + if match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false + then warn_non_primitive_record (mind,0); Declare.declare_univ_binders (IndRef (mind,0)) pl; List.iteri (fun i (indimpls, constrimpls) -> let ind = (mind,i) in @@ -556,8 +556,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls = (ConstructRef (ind, succ j)) impls) constrimpls) impls; - let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in - Flags.if_verbose Feedback.msg_info (minductive_message warn_prim names); + Flags.if_verbose Feedback.msg_info (minductive_message names); if mie.mind_entry_private == None then declare_default_schemes mind; mind |