diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 33b93606ec..5d703011d2 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -22,9 +22,16 @@ open Notation_term (**********************************************************************) (* Utilities *) +(* 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? *) |