diff options
| author | Pierre-Marie Pédrot | 2017-07-04 14:38:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-04 14:52:37 +0200 |
| commit | 8155ba54ae39dd71c6b8ddff2b2b7353dde9aff8 (patch) | |
| tree | 94b2b61cd034873c537b7991cdbe6312fdad2fb3 /interp/notation_ops.ml | |
| parent | 3e0334dd48b5d0b03046d0aff1a82867dc98d656 (diff) | |
| parent | e0ad7ac11b97f089fa862d2e34409e0a1d77d3a1 (diff) | |
Merge branch 'v8.6'
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 1931e81673..5d703011d2 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -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? *) |