aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/egramcoq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/egramcoq.ml')
-rw-r--r--parsing/egramcoq.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index c0ead3a0a..5f63d21c4 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -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 (Ident (Loc.tag ?loc id)))
+ | Name id -> CPatAtom (Some (CAst.make ?loc @@ Ident id))
type 'r env = {
constrs : 'r list;