diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-10-14 10:39:55 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-10-14 10:39:55 +0200 |
| commit | f617aeef08441e83b13f839ce767b840fddbcf7d (patch) | |
| tree | 9a0c914031262f5491745d9773d7c2a0e5bdaa41 /parsing/pcoq.ml4 | |
| parent | ed95f122f3c68becc09c653471dc2982b346d343 (diff) | |
Fix some typos.
Diffstat (limited to 'parsing/pcoq.ml4')
| -rw-r--r-- | parsing/pcoq.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 797b031fe..2e47e07a3 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -298,7 +298,7 @@ module Prim = struct let gec_gen x = make_gen_entry uprim x - (* Entries that can be refered via the string -> Gram.entry table *) + (* Entries that can be referred via the string -> Gram.entry table *) (* Typically for tactic or vernac extensions *) let preident = gec_gen (rawwit wit_pre_ident) "preident" let ident = gec_gen (rawwit wit_ident) "ident" @@ -334,7 +334,7 @@ module Constr = struct let gec_constr = make_gen_entry uconstr (rawwit wit_constr) - (* Entries that can be refered via the string -> Gram.entry table *) + (* Entries that can be referred via the string -> Gram.entry table *) let constr = gec_constr "constr" let operconstr = gec_constr "operconstr" let constr_eoi = eoi_entry constr @@ -367,7 +367,7 @@ module Tactic = (* Main entry for extensions *) let simple_tactic = Gram.entry_create "tactic:simple_tactic" - (* Entries that can be refered via the string -> Gram.entry table *) + (* Entries that can be referred via the string -> Gram.entry table *) (* Typically for tactic user extensions *) let open_constr = make_gen_entry utactic (rawwit wit_open_constr) "open_constr" |