diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-13 00:22:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-18 11:02:58 +0200 |
| commit | 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch) | |
| tree | c0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /interp/genredexpr.ml | |
| parent | f08153148b3ca0de01e5d7c68d5b318a2cae6d0d (diff) | |
Remove reference name type.
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
Diffstat (limited to 'interp/genredexpr.ml')
| -rw-r--r-- | interp/genredexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml index 42c1fe429..607f2258f 100644 --- a/interp/genredexpr.ml +++ b/interp/genredexpr.ml @@ -60,6 +60,6 @@ open Constrexpr type r_trm = constr_expr type r_pat = constr_pattern_expr -type r_cst = reference or_by_notation +type r_cst = qualid or_by_notation type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen |