diff options
Diffstat (limited to 'parsing/egramcoq.ml')
-rw-r--r-- | parsing/egramcoq.ml | 2 |
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; |