diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-27 11:44:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-27 12:40:01 +0100 |
| commit | d51e5688f521c8a77a1dbdb0b88d8f99d5ff8060 (patch) | |
| tree | 3fa5d830feb50a5f96e07c6c4762ac8c3f461189 /toplevel/metasyntax.ml | |
| parent | 73c3dddc94dda003b1bb854d3b6ca9d15474e299 (diff) | |
Finer type for Pcoq.interp_entry_name.
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index ca263e6cb..94b7fe5bc 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -49,8 +49,8 @@ let interp_prod_item lev = function | TacTerm s -> GramTerminal s | TacNonTerm (loc, nt, po) -> let sep = match po with Some (_,sep) -> sep | _ -> "" in - let EntryName (etyp, e) = interp_entry_name true (Some lev) nt sep in - GramNonTerminal (loc, etyp, e, Option.map fst po) + let EntryName (etyp, e) = interp_entry_name true (TgTactic lev) nt sep in + GramNonTerminal (loc, Genarg.unquote etyp, e, Option.map fst po) let make_terminal_status = function | GramTerminal s -> Some s |