diff options
-rw-r--r-- | API/API.mli | 2 | ||||
-rw-r--r-- | interp/implicit_quantifiers.mli | 4 | ||||
-rw-r--r-- | pretyping/typeclasses.ml | 8 | ||||
-rw-r--r-- | pretyping/typeclasses.mli | 5 | ||||
-rw-r--r-- | vernac/classes.ml | 2 | ||||
-rw-r--r-- | vernac/record.ml | 2 |
6 files changed, 11 insertions, 12 deletions
diff --git a/API/API.mli b/API/API.mli index 1a84600ec..6c9ac98ff 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4285,7 +4285,7 @@ sig type typeclass = { cl_univs : Univ.AUContext.t; cl_impl : Globnames.global_reference; - cl_context : (Globnames.global_reference * bool) option list * Context.Rel.t; + cl_context : Globnames.global_reference option list * Context.Rel.t; cl_props : Context.Rel.t; cl_projs : (Names.Name.t * (direction * Vernacexpr.hint_info_expr) option * Names.Constant.t option) list; diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index f7c36c4e5..bfe73160b 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -38,10 +38,10 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits val combine_params_freevar : - Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t -> + Id.Set.t -> global_reference option * Context.Rel.Declaration.t -> Constrexpr.constr_expr * Id.Set.t val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t -> + (Id.Set.t -> global_reference option * Context.Rel.Declaration.t -> Constrexpr.constr_expr * Id.Set.t) -> constr_expr -> constr_expr * Id.Set.t diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 2e213a51d..fc4da8872 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; @@ -175,7 +175,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 +213,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 diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 618826f3d..c1161da0f 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; diff --git a/vernac/classes.ml b/vernac/classes.ml index b80741269..109584436 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -143,7 +143,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false (fun avoid (clname, _) -> match clname with - | Some (cl, b) -> + | Some cl -> let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) diff --git a/vernac/record.ml b/vernac/record.ml index 1d255b08e..6b8753b60 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -520,7 +520,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari let ctx_context = List.map (fun decl -> match Typeclasses.class_of_constr Evd.empty (EConstr.of_constr (RelDecl.get_type decl)) with - | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true) + | Some (_, ((cl,_), _)) -> Some cl.cl_impl | None -> None) params, params in |