From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 20:09:26 +0100 Subject: Eliminating parts of the right-hand side compatibility layer --- pretyping/typeclasses.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'pretyping/typeclasses.ml') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index a970c434f..f59a6dcd9 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -156,17 +156,17 @@ let class_of_constr sigma c = try Some (dest_class_arity (Global.env ()) sigma c) with e when CErrors.noncritical e -> None -let is_class_constr c = - try let gr, u = Universes.global_of_constr c in +let is_class_constr sigma c = + try let gr, u = Termops.global_of_constr sigma c in Refmap.mem gr !classes with Not_found -> false let rec is_class_type evd c = let c, _ = Termops.decompose_app_vect evd c in - match EConstr.kind evd (EConstr.of_constr c) with + match EConstr.kind evd c with | Prod (_, _, t) -> is_class_type evd t | Cast (t, _, _) -> is_class_type evd t - | _ -> is_class_constr c + | _ -> is_class_constr evd c let is_class_evar evd evi = is_class_type evd (EConstr.of_constr evi.Evd.evar_concl) -- cgit v1.2.3