From 15ec807cd201b49ed339d665c34c955a36b29745 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 20 Dec 2019 13:40:02 +0100 Subject: Fix #11140: Bidirectionality hints perform (surprising?) simplification We typecheck arguments like previously, using bidirectionality hints, but ultimately replace them with user-provided arguments on which we replay coercion traces. This is a fix which should be easy to backport, but there are two directions of future work: - Coercion traces for `Program` coercions (in these cases, we currently use the inferred arguments) - Separate the Coercion API in two phases: inference and application of coercions. It will make the approach taken here cleaner, and probably make it easier to interleave typing steps with coercion inference. Co-Authored-By: Gaëtan Gilbert --- proofs/clenv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 58c0f7db53..e466992721 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -678,7 +678,7 @@ let define_with_type sigma env ev c = let t = Retyping.get_type_of env sigma ev in let ty = Retyping.get_type_of env sigma c in let j = Environ.make_judge c ty in - let (sigma, j) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in + let (sigma, j, _trace) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in let (ev, _) = destEvar sigma ev in let sigma = Evd.define ev j.Environ.uj_val sigma in sigma -- cgit v1.2.3