diff options
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 42 |
1 files changed, 26 insertions, 16 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index f405c4d5a9..348e76da62 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -34,17 +34,27 @@ module RelDecl = Context.Rel.Declaration (* 3b| Mutual inductive definitions *) +let warn_auto_template = + CWarnings.create ~name:"auto-template" ~category:"vernacular" + (fun id -> + Pp.(strbrk "Automatically declaring " ++ Id.print id ++ + strbrk " as template polymorphic. Use attributes or " ++ + strbrk "disable Auto Template Polymorphism to avoid this warning.")) + let should_auto_template = let open Goptions in let auto = ref true in - let _ = declare_bool_option + let () = declare_bool_option { optdepr = false; optname = "Automatically make some inductive types template polymorphic"; optkey = ["Auto";"Template";"Polymorphism"]; optread = (fun () -> !auto); optwrite = (fun b -> auto := b); } in - fun () -> !auto + fun id would_auto -> + let b = !auto && would_auto in + if b then warn_auto_template id; + b let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function | CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c) @@ -265,8 +275,8 @@ let inductive_levels env evd poly arities inds = else minlev in let minlev = - (** Indices contribute. *) - if Indtypes.is_indices_matter () && List.length ctx > 0 then ( + (* Indices contribute. *) + if indices_matter env && List.length ctx > 0 then ( let ilev = sign_level env evd ctx in Univ.sup ilev minlev) else minlev @@ -282,15 +292,15 @@ let inductive_levels env evd poly arities inds = let evd, arities = CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len -> if is_impredicative env du then - (** Any product is allowed here. *) + (* Any product is allowed here. *) evd, arity :: arities - else (** If in a predicative sort, or asked to infer the type, - we take the max of: - - indices (if in indices-matter mode) - - constructors - - Type(1) if there is more than 1 constructor + else (* If in a predicative sort, or asked to infer the type, + we take the max of: + - indices (if in indices-matter mode) + - constructors + - Type(1) if there is more than 1 constructor *) - (** Constructors contribute. *) + (* Constructors contribute. *) let evd = if Sorts.is_set du then if not (Evd.check_leq evd cu Univ.type0_univ) then @@ -301,7 +311,7 @@ let inductive_levels env evd poly arities inds = in let evd = if len >= 2 && Univ.is_type0m_univ cu then - (** "Polymorphic" type constraint and more than one constructor, + (* "Polymorphic" type constraint and more than one constructor, should not land in Prop. Add constraint only if it would land in Prop directly (no informative arguments as well). *) Evd.set_leq_sort env evd Set du @@ -402,7 +412,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let env_ar_params = EConstr.push_rel_context ctx_params env_ar in (* Try further to solve evars, and instantiate them *) - let sigma = solve_remaining_evars all_and_fail_flags env_params sigma (Evd.from_env env_params) in + let sigma = solve_remaining_evars all_and_fail_flags env_params sigma in (* Compute renewed arities *) let sigma = Evd.minimize_universes sigma in let nf = Evarutil.nf_evars_universes sigma in @@ -431,8 +441,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); template | None -> - should_auto_template () && not poly && - Option.cata (fun s -> not (Sorts.is_small s)) false concl + should_auto_template ind.ind_name (not poly && + Option.cata (fun s -> not (Sorts.is_small s)) false concl) in { mind_entry_typename = ind.ind_name; mind_entry_arity = arity; @@ -510,7 +520,7 @@ let is_recursive mie = let rec is_recursive_constructor lift typ = match Constr.kind typ with | Prod (_,arg,rest) -> - not (EConstr.Vars.noccurn Evd.empty (** FIXME *) lift (EConstr.of_constr arg)) || + not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) || is_recursive_constructor (lift+1) rest | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest | _ -> false |