From 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 13 Jun 2018 00:22:57 +0200
Subject: 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.
---
 interp/genredexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/genredexpr.ml')

diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml
index 42c1fe429b..607f2258fd 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
-- 
cgit v1.2.3