diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-21 17:52:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-21 18:30:53 +0200 |
| commit | 1b2a1f0229b485496497ebd1ddbbc561825d61e6 (patch) | |
| tree | 012a2d7c49ccdc42d7c538ba3b37eb45e862753b /grammar/vernacextend.ml4 | |
| parent | 513344627bbdf4d822ca93156d2e2943408ec50d (diff) | |
Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.
Diffstat (limited to 'grammar/vernacextend.ml4')
| -rw-r--r-- | grammar/vernacextend.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 03061d8bd..d99af6a33 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -181,10 +181,10 @@ EXTEND ; args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let t, g = interp_entry_name false None e "" in + let EntryName (t, g) = interp_entry_name false None e "" in GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let t, g = interp_entry_name false None e sep in + let EntryName (t, g) = interp_entry_name false None e sep in GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) | s = STRING -> GramTerminal s |