diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index c46e5e9da..b6e62e445 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -47,9 +47,16 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with | GHole _ | GSort _ | GLetIn _), _ -> false +(* helper for NVar, NVar case in eq_notation_constr *) +let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None + let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | NRef gr1, NRef gr2 -> eq_gr gr1 gr2 -| NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2) +| NVar id1, NVar id2 -> ( + match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with + | Some n,Some m -> Int.equal n m + | None ,None -> Id.equal id1 id2 + | _ -> false) | NApp (t1, a1), NApp (t2, a2) -> (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2 | NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *) |