diff options
| author | Pierre-Marie Pédrot | 2015-10-15 09:47:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-15 09:47:43 +0200 |
| commit | cbd28511526dfb561017c3d27a73598f6ce5f68d (patch) | |
| tree | a8786b32433caa850e24f67ab5a3aa85f29a683a /parsing | |
| parent | 10e5883fed21f9631e1aa65adb7a7e62a529987f (diff) | |
| parent | 7402a7788b6a73bd5c0cb9078823d48e6f01a357 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/lexer.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 8e83929619..c6d5f3b925 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -70,7 +70,7 @@ let ttree_remove ttree str = remove ttree 0 -(* Errors occuring while lexing (explained as "Lexer error: ...") *) +(* Errors occurring while lexing (explained as "Lexer error: ...") *) module Error = struct diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 797b031fe4..2e47e07a36 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" |