diff options
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index d6a6162f9..a6fb48749 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -22,6 +22,8 @@ open Constrintern open Constrexpr open Sigma.Notations open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (*i*) open Decl_kinds @@ -77,13 +79,13 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m let type_ctx_instance evars env ctx inst subst = let rec aux (subst, instctx) l = function decl :: ctx -> - let t' = substl subst (get_type decl) in + let t' = substl subst (RelDecl.get_type decl) in let c', l = match decl with | LocalAssum _ -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l | LocalDef (_,b,_) -> substl subst b, l in - let d = get_name decl, Some c', t' in + let d = RelDecl.get_name decl, Some c', t' in aux (c' :: subst, d :: instctx) l ctx | [] -> subst in aux (subst, []) inst (List.rev ctx) @@ -156,7 +158,6 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let cl, u = Typeclasses.typeclass_univ_instance k in let _, args = List.fold_right (fun decl (args, args') -> - let open Context.Rel.Declaration in match decl with | LocalAssum _ -> (List.tl args, List.hd args :: args') | LocalDef (_,b,_) -> (args, substl args' b :: args')) @@ -229,7 +230,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p (fun (props, rest) decl -> if is_local_assum decl then try - let is_id (id', _) = match get_name decl, get_id id' with + let is_id (id', _) = match RelDecl.get_name decl, get_id id' with | Name id, (_, id') -> Id.equal id id' | Anonymous, _ -> false in @@ -347,7 +348,7 @@ let named_of_rel_context l = let acc, ctx = List.fold_right (fun decl (subst, ctx) -> - let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in + let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in let d = match decl with | LocalAssum (_,t) -> id, None, substl subst t | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in |