diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-03-25 01:42:38 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-03-25 01:43:59 +0100 |
| commit | 25c6356326773ac56380b81de6f58d15caae8680 (patch) | |
| tree | 31bc5b3341bd8addc930aea23e67f2f3c6791377 | |
| parent | a6d6bca5f024cbdc35924c2cb5e399eb8a2d9c16 (diff) | |
Fix a bug in Program coercion code
It was not accounting for the universe constraints generated by
applications of the coercion.
| -rw-r--r-- | pretyping/coercion.ml | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 489a311bc..d00445958 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -129,7 +129,7 @@ let mu env evdref t = let rec aux v = let v' = hnf env !evdref v in match disc_subset v' with - Some (u, p) -> + | Some (u, p) -> let f, ct = aux u in let p = hnf_nodelta env !evdref p in (Some (fun x -> @@ -241,7 +241,6 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let remove_head a c = match kind_of_term c with | Lambda (n, t, t') -> c, t' - (*| Prod (n, t, t') -> t'*) | Evar (k, args) -> let (evs, t) = Evarutil.define_evar_as_lambda env !evdref (k,args) in evdref := evs; @@ -297,9 +296,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) with NoSubtacCoercion -> let typ = Typing.unsafe_type_of env evm c in let typ' = Typing.unsafe_type_of env evm c' in - (* if not (is_arity env evm typ) then *) coerce_application typ typ' c c' l l') - (* else subco () *) else subco () | x, y when Constr.equal c c' -> @@ -307,9 +304,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let evm = !evdref in let lam_type = Typing.unsafe_type_of env evm c in let lam_type' = Typing.unsafe_type_of env evm c' in - (* if not (is_arity env evm lam_type) then ( *) coerce_application lam_type lam_type' c c' l l' - (* ) else subco () *) else subco () | _ -> subco ()) | _, _ -> subco () @@ -335,10 +330,17 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) raise NoSubtacCoercion in coerce_unify env x y +let app_coercion env evdref coercion v = + match coercion with + | None -> v + | Some f -> + let v' = Typing.solve_evars env evdref (f v) in + whd_betaiota !evdref v' + let coerce_itf loc env evd v t c1 = let evdref = ref evd in let coercion = coerce loc env evdref t c1 in - let t = Option.map (app_opt env evdref coercion) v in + let t = Option.map (app_coercion env evdref coercion) v in !evdref, t let saturate_evd env evd = @@ -424,7 +426,7 @@ let inh_coerce_to_base loc env evd j = let evdref = ref evd in let ct, typ' = mu env evdref j.uj_type in let res = - { uj_val = app_opt env evdref ct j.uj_val; + { uj_val = app_coercion env evdref ct j.uj_val; uj_type = typ' } in !evdref, res else (evd, j) |