diff options
Diffstat (limited to 'contrib/subtac/subtac_coercion.ml')
| -rw-r--r-- | contrib/subtac/subtac_coercion.ml | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 4a9cf8eb47..cdad003721 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -97,7 +97,7 @@ module Coercion = struct app_opt f (mkApp ((Lazy.force sig_).proj1, [| u; p; x |]))), ct) - | None -> (None, t) + | None -> (None, v) in aux t and coerce loc env isevars (x : Term.constr) (y : Term.constr) @@ -153,7 +153,7 @@ module Coercion = struct if i = Term.destInd existS.typ then begin - debug 1 (str "In coerce sigma types"); + trace (str "In coerce sigma types"); let (a, pb), (a', pb') = pair_of_array l, pair_of_array l' in @@ -339,6 +339,13 @@ module Coercion = struct | _ -> inh_tosort_force loc env isevars j + let inh_coerce_to_base loc env isevars j = + let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in + let ct, typ' = mu env isevars typ in + isevars, { uj_val = app_opt ct j.uj_val; + uj_type = typ' } + + let inh_coerce_to_fail env isevars c1 v t = let v', t' = try |