diff options
| author | Maxime Dénès | 2019-12-20 13:40:02 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2020-01-06 22:48:38 +0100 |
| commit | 15ec807cd201b49ed339d665c34c955a36b29745 (patch) | |
| tree | f90d7c4f3b7e3156dda9b89dd802570fd68d0816 /pretyping/cases.ml | |
| parent | a7de863bf68f6aae3832e8c8d5b000576d107a63 (diff) | |
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 <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index aa6ec1c941..cbd04a76ad 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -436,7 +436,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = | exception Evarconv.UnableToUnify _ -> sigma, current | sigma -> sigma, current else - let sigma, j = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in + let sigma, j, _trace = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in sigma, j.uj_val in sigma, (current, try_find_ind !!(pb.env) sigma indt names)) @@ -1955,8 +1955,12 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let inh_conv_coerce_to_tycon ?loc ~program_mode env sigma j tycon = match tycon with - | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma - ~flags:(default_flags_of TransparentState.full) j p + | Some p -> + let (evd,v,_trace) = + Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma + ~flags:(default_flags_of TransparentState.full) j p + in + (evd,v) | None -> sigma, j (* We put the tycon inside the arity signature, possibly discovering dependencies. *) |