diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/glob_ops.ml | 9 | ||||
| -rw-r--r-- | pretyping/glob_term.ml | 1 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 3 |
3 files changed, 3 insertions, 10 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 86d2cc78e0..5a8ac32ffa 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -104,9 +104,8 @@ let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with let cast_type_eq eq t1 t2 = match t1, t2 with | CastConv t1, CastConv t2 -> eq t1 t2 | CastVM t1, CastVM t2 -> eq t1 t2 - | CastCoerce, CastCoerce -> true | CastNative t1, CastNative t2 -> eq t1 t2 - | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> false + | (CastConv _ | CastVM _ | CastNative _), _ -> false let matching_var_kind_eq k1 k2 = match k1, k2 with | FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2 @@ -188,14 +187,12 @@ let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c let map_cast_type f = function | CastConv a -> CastConv (f a) | CastVM a -> CastVM (f a) - | CastCoerce -> CastCoerce | CastNative a -> CastNative (f a) let smartmap_cast_type f c = match c with | CastConv a -> let a' = f a in if a' == a then c else CastConv a' | CastVM a -> let a' = f a in if a' == a then c else CastVM a' - | CastCoerce -> CastCoerce | CastNative a -> let a' = f a in if a' == a then c else CastNative a' let map_glob_constr_left_to_right f = DAst.map (function @@ -275,7 +272,7 @@ let fold_glob_constr f acc = DAst.with_val (function Array.fold_left f (Array.fold_left f acc tyl) bv | GCast (c,k) -> let acc = match k with - | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in + | CastConv t | CastVM t | CastNative t -> f acc t in f acc c | GArray (_u,t,def,ty) -> f (f (Array.fold_left f acc t) def) ty | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc @@ -318,7 +315,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function Array.fold_left_i f' acc idl | GCast (c,k) -> let acc = match k with - | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in + | CastConv t | CastVM t | CastNative t -> f v acc t in f v acc c | GArray (_u, t, def, ty) -> f v (f v (Array.fold_left (f v) acc t) def) ty | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc)) diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 9f93e5e6c1..d480c12834 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -57,7 +57,6 @@ and glob_fix_kind = type 'a cast_type = | CastConv of 'a | CastVM of 'a - | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) | CastNative of 'a (** The kind of patterns that occurs in "match ... with ... end" diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index de1af62043..cb52e32cd5 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1165,9 +1165,6 @@ struct let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let sigma, cj = match k with - | CastCoerce -> - let sigma, cj = pretype empty_tycon env sigma c in - Coercion.inh_coerce_to_base ?loc ~program_mode !!env sigma cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in let sigma, tj = eval_type_pretyper self ~program_mode ~poly resolve_tc empty_valcon env sigma t in |