diff options
| author | Emilio Jesus Gallego Arias | 2019-06-17 12:28:14 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:28:14 +0200 |
| commit | 5d18dfed8e68dd964bca5d64ca6bdd9f8ffbb1df (patch) | |
| tree | 705d949f1b8ac657d88d4a650d13ed3c7210e495 /vernac/classes.ml | |
| parent | 6c53049049781a71e366edd738747f9b30eb5d94 (diff) | |
| parent | 1e3ca892b208c22956d6c8f89a1d5863711d0cd9 (diff) | |
Merge PR #10231: Adding location in warning telling implicit arguments differ in term and type
Reviewed-by: ejgallego
Ack-by: jashug
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index b64af52b6e..bd5a211f1d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -537,8 +537,7 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass = in let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in let sigma, (c', imps') = interp_type_evars_impls ~program_mode ~impls env' sigma tclass in - let len = Context.Rel.nhyps ctx in - let imps = imps @ Impargs.lift_implicits len imps' in + let imps = imps @ imps' in let ctx', c = decompose_prod_assum sigma c' in let ctx'' = ctx' @ ctx in let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in |