diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-20 20:09:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:34 +0100 |
| commit | d4b344acb23f19b089098b7788f37ea22bc07b81 (patch) | |
| tree | 6dd26d747b259793ef6a24befd27e13234b19875 /pretyping/typeclasses.ml | |
| parent | 2cd0648e003308a000f9f89c898bce4d15fc94a1 (diff) | |
Eliminating parts of the right-hand side compatibility layer
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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) |