diff options
| author | Hugo Herbelin | 2020-09-27 10:46:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-10 22:16:39 +0200 |
| commit | a6d52d2502c09e8acdca464faf67d3956448cbcf (patch) | |
| tree | 71bf5602781c1e21a90d84555d8b62068fc31149 /parsing/pcoq.ml | |
| parent | b7c9ba2c678228593450ecdf272ff71facbc6a6e (diff) | |
Prim.pattern_ident takes a location and its synonymous pattern_identref is deprecated.
Diffstat (limited to 'parsing/pcoq.ml')
| -rw-r--r-- | parsing/pcoq.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 723f08413e..fa7de40a30 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -286,7 +286,7 @@ module Prim = let univ_decl = Entry.create "univ_decl" let ident_decl = Entry.create "ident_decl" let pattern_ident = Entry.create "pattern_ident" - let pattern_identref = Entry.create "pattern_identref" + let pattern_identref = pattern_ident (* To remove in 8.14 *) (* A synonym of ident - maybe ident will be located one day *) let base_ident = Entry.create "base_ident" |