diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 19:21:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 20:41:05 +0200 |
| commit | 02b66da78e766a0eb8a1ec82a03ec9ce5418a0f0 (patch) | |
| tree | 1d157ece2d488deaa419fbd12901ad56a2f807aa /pretyping/coercion.ml | |
| parent | 8c32ecc205aebaf9a4da95e24463286aee1a571d (diff) | |
Fix bug #3672, application of primitive projections as coercions.
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 0ae873643..0ec25d402 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -47,11 +47,21 @@ exception NoCoercion exception NoCoercionNoUnifier of evar_map * unification_error (* Here, funj is a coercion therefore already typed in global context *) -let apply_coercion_args env evd check argl funj = +let apply_coercion_args env evd check isproj argl funj = let evdref = ref evd in let rec apply_rec acc typ = function - | [] -> { uj_val = applist (j_val funj,argl); - uj_type = typ } + | [] -> + if isproj then + let cst = fst (destConst (j_val funj)) in + let p = Projection.make cst false in + let pb = lookup_projection p env in + let args = List.skipn pb.Declarations.proj_npars argl in + let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in + { uj_val = applist (mkProj (p, hd), tl); + uj_type = typ } + else + { uj_val = applist (j_val funj,argl); + uj_type = typ } | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *) match kind_of_term (whd_betadeltaiota env evd typ) with | Prod (_,c1,c2) -> @@ -345,13 +355,10 @@ let apply_coercion env sigma p hj typ_cl = let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in let sigma, jres = - apply_coercion_args env sigma true argl fv + apply_coercion_args env sigma true isproj argl fv in (if isid then { uj_val = ja.uj_val; uj_type = jres.uj_type } - else if isproj then - { uj_val = mkProj (Projection.make (fst (destConst fv.uj_val)) false, ja.uj_val); - uj_type = jres.uj_type } else jres), jres.uj_type,sigma) |