diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 6 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 14 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 7 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 |
5 files changed, 14 insertions, 17 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f7a3789a21..788e4d268a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1044,7 +1044,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite -> + | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite -> let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 34df7d3d72..78e6bc6f14 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -275,7 +275,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p let has_dependent_elim mib = match mib.mind_record with - | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite + | Some (Some _) -> mib.mind_finite == BiFinite | _ -> true (* Annotation for cases *) @@ -486,7 +486,7 @@ let find_inductive env sigma c = let (t, l) = decompose_app sigma (whd_all env sigma c) in match EConstr.kind sigma t with | Ind ind - when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite -> + when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> CoFinite -> let l = List.map EConstr.Unsafe.to_constr l in (ind, l) | _ -> raise Not_found @@ -496,7 +496,7 @@ let find_coinductive env sigma c = let (t, l) = decompose_app sigma (whd_all env sigma c) in match EConstr.kind sigma t with | Ind ind - when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite -> + when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == CoFinite -> let l = List.map EConstr.Unsafe.to_constr l in (ind, l) | _ -> raise Not_found diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index bbb3a1bb2b..f153b63410 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -65,7 +65,7 @@ type typeclass = { cl_impl : global_reference; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : (global_reference * bool) option list * Context.Rel.t; + cl_context : global_reference option list * Context.Rel.t; (* Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; @@ -87,7 +87,6 @@ type instance = { (* Sections where the instance should be redeclared, None for discard, Some 0 for none. *) is_global: int option; - is_poly: bool; is_impl: global_reference; } @@ -97,7 +96,7 @@ let instance_impl is = is.is_impl let hint_priority is = is.is_info.Vernacexpr.hint_priority -let new_instance cl info glob poly impl = +let new_instance cl info glob impl = let global = if glob then Some (Lib.sections_depth ()) else None @@ -107,7 +106,6 @@ let new_instance cl info glob poly impl = { is_class = cl.cl_impl; is_info = info ; is_global = global ; - is_poly = poly; is_impl = impl } (* @@ -175,7 +173,7 @@ let subst_class (subst,cl) = and do_subst_gr gr = fst (subst_global subst gr) in let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = - List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs, + List.smartmap (Option.smartmap do_subst_gr) grs, do_subst_ctx ctx in let do_subst_projs projs = List.smartmap (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in @@ -213,10 +211,10 @@ let discharge_class (_,cl) = let newgrs = List.map (fun decl -> match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr Evd.empty with | None -> None - | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true)) + | Some (_, ((tc,_), _)) -> Some tc.cl_impl) ctx' in - List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs + List.smartmap (Option.smartmap Lib.discharge_global) grs @ newgrs in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in @@ -420,7 +418,7 @@ let declare_instance info local glob = match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> assert (not (isVarRef glob) || local); - add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob) + add_instance (new_instance tc info (not local) glob) | None -> () let add_class cl = diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 8ee061330a..ee28ec173b 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -25,9 +25,8 @@ type typeclass = { cl_impl : global_reference; (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. - The boolean indicates if the typeclass argument is a direct superclass and the global reference - gives a direct link to the class itself. *) - cl_context : (global_reference * bool) option list * Context.Rel.t; + The global reference gives a direct link to the class itself. *) + cl_context : global_reference option list * Context.Rel.t; (** Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; @@ -54,7 +53,7 @@ val all_instances : unit -> instance list val add_class : typeclass -> unit -val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic -> +val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> global_reference -> instance val add_instance : instance -> unit val remove_instance : instance -> unit diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 30674fee27..b41fb4e4dd 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -666,7 +666,7 @@ let is_eta_constructor_app env sigma ts f l1 term = | Construct (((_, i as ind), j), u) when i == 0 && j == 1 -> let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite && + | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite && Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> (** Check that the other term is neutral *) is_neutral env sigma ts term |