diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-14 22:36:47 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-04 22:29:03 +0200 |
| commit | afceace455a4b37ced7e29175ca3424996195f7b (patch) | |
| tree | a76a6acc9e3210720d0920c4341a798eecdd3f18 /interp/notation_ops.ml | |
| parent | af19d08003173718c0f7c070d0021ad958fbe58d (diff) | |
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index a76f82094..6a282624e 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -28,7 +28,7 @@ open Notation_term 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 +| NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2 | NVar id1, NVar id2 -> ( match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with | Some n,Some m -> Int.equal n m @@ -1123,7 +1123,7 @@ let rec match_ inner u alp metas sigma a1 a2 = (* Matching compositionally *) | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma - | GRef (r1,_), NRef r2 when (eq_gr r1 r2) -> sigma + | GRef (r1,_), NRef r2 when (GlobRef.equal r1 r2) -> sigma | GApp (f1,l1), NApp (f2,l2) -> let n1 = List.length l1 and n2 = List.length l2 in let f1,l1,f2,l2 = |