diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/subtac_cases.ml | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac_coercion.ml | 19 |
2 files changed, 10 insertions, 11 deletions
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 5e574ce538..4f8344745e 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -1576,7 +1576,7 @@ let constr_of_pat env isevars arsign pat avoid = in let neq = eq_id avoid id in (Name neq, Some (mkRel 0), eq_t) :: sign, 2, neq :: avoid - with NotUnifiable _ -> sign, 1, avoid + with Reduction.NotConvertible -> sign, 1, avoid in (* Mark the equality as a hole *) pat', sign, lift i app, lift i apptype, realargs, n + i, avoid diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index 2610ed4ed7..5a2d840570 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -112,7 +112,7 @@ module Coercion = struct try isevars := the_conv_x_leq env x y !isevars; None - with NotUnifiable _ -> coerce' env x y + with Reduction.NotConvertible -> coerce' env x y and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env isevars x y in let dest_prod c = @@ -129,12 +129,12 @@ module Coercion = struct let (n, eqT), restT = dest_prod typ in let (n', eqT'), restT' = dest_prod typ' in aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co - with NotUnifiable _ -> + with Reduction.NotConvertible -> let (n, eqT), restT = dest_prod typ in let (n', eqT'), restT' = dest_prod typ' in let _ = try isevars := the_conv_x_leq env eqT eqT' !isevars - with NotUnifiable _ -> raise NoSubtacCoercion + with Reduction.NotConvertible -> raise NoSubtacCoercion in (* Disallow equalities on arities *) if Reduction.is_arity env eqT then raise NoSubtacCoercion; @@ -323,7 +323,6 @@ module Coercion = struct (* appliquer le chemin de coercions de patterns p *) exception NoCoercion - exception NoCoercionNoUnifier of evar_map * unification_error let apply_pattern_coercion loc pat p = List.fold_left @@ -419,12 +418,12 @@ module Coercion = struct with Not_found -> raise NoCoercion in try (the_conv_x_leq env t' c1 evd, v') - with NotUnifiable _ -> raise NoCoercion + with Reduction.NotConvertible -> raise NoCoercion let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = try (the_conv_x_leq env t c1 evd, v) - with NotUnifiable (best_failed_evd,e) -> + with Reduction.NotConvertible -> try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> match @@ -448,7 +447,7 @@ module Coercion = struct let t2 = Termops.subst_term v1 t2 in let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') - | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) + | _ -> raise NoCoercion (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) = @@ -459,12 +458,12 @@ module Coercion = struct inh_conv_coerce_to_fail loc env evd rigidonly (Some (nf_evar evd cj.uj_val)) (nf_evar evd cj.uj_type) (nf_evar evd t) - with NoCoercionNoUnifier (best_failed_evd,e) -> + with NoCoercion -> let sigma = evd in try coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t with NoSubtacCoercion -> - error_actual_type_loc loc env sigma cj t e + error_actual_type_loc loc env sigma cj t in let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) @@ -491,7 +490,7 @@ module Coercion = struct in try fst (try inh_conv_coerce_to_fail loc env' isevars false None t t' - with NoCoercionNoUnifier _ -> + with NoCoercion -> coerce_itf loc env' isevars None t t') with NoSubtacCoercion -> error_cannot_coerce env' isevars (t, t')) |