diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 2 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 3 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 6 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 4 | ||||
| -rw-r--r-- | vernac/record.ml | 4 |
5 files changed, 9 insertions, 10 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 51dd5cd4f..ec6b62ee2 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -317,7 +317,7 @@ let build_beq_scheme mode kn = let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in if not (Sorts.List.mem InSet kelim) then raise (NonSingletonProp (kn,i)); - if mib.mind_finite = Decl_kinds.CoFinite then + if mib.mind_finite = CoFinite then raise NoDecidabilityCoInductive; let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in create_input fix), diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index f3f50f41d..1c8677e9c 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -25,7 +25,6 @@ open Nametab open Impargs open Reductionops open Indtypes -open Decl_kinds open Pretyping open Evarutil open Indschemes @@ -411,7 +410,7 @@ 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 *) begin match mie.mind_entry_finite with - | BiFinite when is_recursive mie -> + | Declarations.BiFinite when is_recursive mie -> if Option.has_some mie.mind_entry_record then user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") else diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index e4ca98749..2f4c95aff 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -258,7 +258,7 @@ let declare_one_induction_scheme ind = let declare_induction_schemes kn = let mib = Global.lookup_mind kn in - if mib.mind_finite <> Decl_kinds.CoFinite then begin + if mib.mind_finite <> Declarations.CoFinite then begin for i = 0 to Array.length mib.mind_packets - 1 do declare_one_induction_scheme (kn,i); done; @@ -268,7 +268,7 @@ let declare_induction_schemes kn = let declare_eq_decidability_gen internal names kn = let mib = Global.lookup_mind kn in - if mib.mind_finite <> Decl_kinds.CoFinite then + if mib.mind_finite <> Declarations.CoFinite then ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn) let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *) @@ -512,7 +512,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) + if !elim_flag && (mib.mind_finite <> Declarations.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; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 27a680b9b..6ef310837 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -100,7 +100,7 @@ let find_mutually_recursive_statements sigma thms = match EConstr.kind sigma t with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in - mind.mind_finite <> Decl_kinds.CoFinite -> + mind.mind_finite <> Declarations.CoFinite -> [ind,x,i] | _ -> []) 0 (List.rev (List.filter Context.Rel.Declaration.is_local_assum whnf_hyp_hds))) in @@ -110,7 +110,7 @@ let find_mutually_recursive_statements sigma thms = match EConstr.kind sigma whnf_ccl with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in - Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite -> + Int.equal mind.mind_ntypes n && mind.mind_finite == Declarations.CoFinite -> [ind,x,0] | _ -> [] in diff --git a/vernac/record.ml b/vernac/record.ml index 114b55cb4..fb73f3a01 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -143,7 +143,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in let assums = List.filter is_local_assum newps in let params = List.map (RelDecl.get_name %> Name.get_id) assums in - let ty = Inductive (params,(finite != BiFinite)) in + let ty = Inductive (params,(finite != Declarations.BiFinite)) in let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr sigma arity] [imps] in let env2,sigma,impls,newfs,data = interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) @@ -507,7 +507,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari | Monomorphic_const_entry univs -> Monomorphic_ind_entry univs in - let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls + let ind = declare_structure Declarations.BiFinite ubinders univs (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in |