aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/egramcoq.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-13 00:22:57 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-18 11:02:58 +0200
commit61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch)
treec0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /vernac/egramcoq.ml
parentf08153148b3ca0de01e5d7c68d5b318a2cae6d0d (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 'vernac/egramcoq.ml')
-rw-r--r--vernac/egramcoq.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 434e836d8..cc9be7b0e 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -229,7 +229,7 @@ type prod_info = production_level * production_position
type (_, _) entry =
| TTName : ('self, lname) entry
-| TTReference : ('self, reference) entry
+| TTReference : ('self, qualid) entry
| TTBigint : ('self, Constrexpr.raw_natural_number) entry
| TTConstr : prod_info * 'r target -> ('r, 'r) entry
| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
@@ -312,7 +312,7 @@ let interp_entry forpat e = match e with
let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with
| Anonymous -> CPatAtom None
- | Name id -> CPatAtom (Some (CAst.make ?loc @@ Ident id))
+ | Name id -> CPatAtom (Some (qualid_of_ident ?loc id))
type 'r env = {
constrs : 'r list;