diff options
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 618ec2bc0c..fbabaa4328 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -63,7 +63,7 @@ let existing_instance glob g = let mismatched_params env n m = mismatched_ctx_inst env Parameters n m let mismatched_props env n m = mismatched_ctx_inst env Properties n m -type binder_list = (identifier Loc.located * bool * constr_expr) list +type binder_list = (Id.t Loc.located * bool * constr_expr) list (* Declare everything in the parameters as implicit, and the class instance as well *) @@ -121,7 +121,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props let tclass, ids = match bk with | Implicit -> - Implicit_quantifiers.implicit_application Idset.empty ~allow_partial:false + Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false (fun avoid (clname, (id, _, t)) -> match clname with | Some (cl, b) -> @@ -129,7 +129,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl - | Explicit -> cl, Idset.empty + | Explicit -> cl, Id.Set.empty in let tclass = if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass) else tclass in let k, cty, ctx', ctx, len, imps, subst = @@ -210,7 +210,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props if Option.is_empty b then try let is_id (id', _) = match id, get_id id' with - | Name id, (_, id') -> id_eq id id' + | Name id, (_, id') -> Id.equal id id' | Anonymous, _ -> false in let (loc_mid, c) = @@ -338,7 +338,7 @@ let context l = else ( let impl = List.exists (fun (x,_) -> - match x with ExplByPos (_, Some id') -> id_eq id id' | _ -> false) impls + match x with ExplByPos (_, Some id') -> Id.equal id id' | _ -> false) impls in Command.declare_assumption false (Local (* global *), Definitional) t [] impl (* implicit *) None (* inline *) (Loc.ghost, id) && status) |