diff options
| -rw-r--r-- | contrib/subtac/interp.ml | 2 | ||||
| -rw-r--r-- | contrib/subtac/subtac_coercion.ml | 3 |
2 files changed, 2 insertions, 3 deletions
diff --git a/contrib/subtac/interp.ml b/contrib/subtac/interp.ml index 1be49ef275..83f26ced1e 100644 --- a/contrib/subtac/interp.ml +++ b/contrib/subtac/interp.ml @@ -268,7 +268,7 @@ let rec pretype tycon env isevars lvar = function let resj = evd_comb1 (inh_app_fun env) isevars resj in let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in - let coercef, resty = Subtac_coercion.mu env isevars resj in + let coercef, resty = Subtac_coercion.mu env isevars resty in match kind_of_term resty with | Prod (na,c1,c2) -> let hj = pretype (mk_tycon c1) env isevars lvar c in diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index c1996953bb..fa5dc5bec7 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -84,8 +84,7 @@ let sort_rel s1 s2 = | Type _, Prop Null -> Prop Null | _, Type _ -> s2 -let rec mu env isevars j = - let {uj_val = v; uj_type = t} = j in +let rec mu env isevars t = let rec aux v = match disc_subset v with Some (u, p) -> |