diff options
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 6e01a676a..8c43ac8b5 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -32,6 +32,8 @@ open Misctypes open Proofview.Notations open Hints +module NamedDecl = Context.Named.Declaration + (** Hint database named "typeclass_instances", now created directly in Auto *) (** Options handling *) @@ -523,9 +525,8 @@ let evars_to_goals p evm = (** Making local hints *) let make_resolve_hyp env sigma st flags only_classes pri decl = - let open Context.Named.Declaration in - let id = get_id decl in - let cty = Evarutil.nf_evar sigma (get_type decl) in + let id = NamedDecl.get_id decl in + let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in let rec iscl env ty = let ctx, ar = decompose_prod_assum ty in match kind_of_term (fst (decompose_app ar)) with @@ -564,10 +565,9 @@ let make_hints g st only_classes sign = List.fold_left (fun hints hyp -> let consider = - let open Context.Named.Declaration in - try let t = Global.lookup_named (get_id hyp) |> get_type in + try let t = Global.lookup_named (NamedDecl.get_id hyp) |> NamedDecl.get_type in (* Section variable, reindex only if the type changed *) - not (Term.eq_constr t (get_type hyp)) + not (Term.eq_constr t (NamedDecl.get_type hyp)) with Not_found -> true in if consider then |