diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 5 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 8 |
2 files changed, 3 insertions, 10 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index f02874253e..40fe13784a 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -261,11 +261,9 @@ and cast_expr_eq c1 c2 = match c1, c2 with | CastConv t1, CastConv t2 | CastVM t1, CastVM t2 | CastNative t1, CastNative t2 -> constr_expr_eq t1 t2 -| CastCoerce, CastCoerce -> true | CastConv _, _ | CastVM _, _ -| CastNative _, _ -| CastCoerce, _ -> false +| CastNative _, _ -> false let constr_loc c = CAst.(c.loc) let cases_pattern_expr_loc cp = CAst.(cp.loc) @@ -343,7 +341,6 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function | CLetIn (na,a,t,b) -> f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b - | CCast (a,CastCoerce) -> f n acc a | CNotation (_,_,(l,ll,bl,bll)) -> (* The following is an approximation: we don't know exactly if an ident is binding nor to which subterms bindings apply *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ea5e2a1ad4..ea95655c18 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -35,9 +35,8 @@ let rec alpha_var id1 id2 = function let cast_type_iter2 f t1 t2 = match t1, t2 with | CastConv t1, CastConv t2 -> f t1 t2 | CastVM t1, CastVM t2 -> f t1 t2 - | CastCoerce, CastCoerce -> () | CastNative t1, CastNative t2 -> f t1 t2 - | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> raise Exit + | (CastConv _ | CastVM _ | CastNative _), _ -> raise Exit (* used to update the notation variable with the local variables used in NList and NBinderList, since the iterator has its own variable *) @@ -1319,12 +1318,9 @@ let match_cast match_fun sigma c1 c2 = | CastVM t1, CastVM t2 | CastNative t1, CastNative t2 -> match_fun sigma t1 t2 - | CastCoerce, CastCoerce -> - sigma | CastConv _, _ | CastVM _, _ - | CastNative _, _ - | CastCoerce, _ -> raise No_match + | CastNative _, _ -> raise No_match let does_not_come_from_already_eta_expanded_var glob = (* This is hack to avoid looping on a rule with rhs of the form *) |