diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-24 17:15:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:38 +0100 |
| commit | 531590c223af42c07a93142ab0cea470a98964e6 (patch) | |
| tree | bfe531d8d32e491a66eceba60995702e20e73757 /pretyping/typeclasses.ml | |
| parent | b36adb2124d3ba8a5547605e7f89bb0835d0ab10 (diff) | |
Removing compatibility layers in Retyping
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 9ee34341b..9da7005e0 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -270,7 +270,7 @@ let add_class cl = let check_instance env sigma c = try let (evd, c) = resolve_one_typeclass env sigma - (EConstr.of_constr (Retyping.get_type_of env sigma c)) in + (Retyping.get_type_of env sigma c) in not (Evd.has_undefined evd) with e when CErrors.noncritical e -> false @@ -314,7 +314,7 @@ let build_subclasses ~check env sigma glob pri = let declare_proj hints (cref, pri, body) = let path' = cref :: path in let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in - let rest = aux pri body (EConstr.of_constr ty) path' in + let rest = aux pri body ty path' in hints @ (path', pri, body) :: rest in List.fold_left declare_proj [] projs in |