diff options
Diffstat (limited to 'cparser/validator/Grammar.v')
| -rw-r--r-- | cparser/validator/Grammar.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/cparser/validator/Grammar.v b/cparser/validator/Grammar.v index d162892d..0768d647 100644 --- a/cparser/validator/Grammar.v +++ b/cparser/validator/Grammar.v @@ -96,8 +96,8 @@ Module Defs(Import G:T). Definition token := {t:terminal & symbol_semantic_type (T t)}. (** A grammar creates a relation between word of tokens and semantic values. - This relation is parametrized by the head symbol. It defines the - "semantics" of the grammar. This relation is defined by a notion of + This relation is parametrized by the head symbol. It defines the + "semantics" of the grammar. This relation is defined by a notion of parse tree. **) Inductive parse_tree: forall (head_symbol:symbol) (word:list token) @@ -110,9 +110,9 @@ Module Defs(Import G:T). parse_tree (T t) [existT (fun t => symbol_semantic_type (T t)) t sem] sem - (** Given a production, if a word has a list of semantic values for the - right hand side as head symbols, then this word has the semantic value - given by the semantic action of the production for the left hand side + (** Given a production, if a word has a list of semantic values for the + right hand side as head symbols, then this word has the semantic value + given by the semantic action of the production for the left hand side as head symbol.**) | Non_terminal_pt: forall {p:production} {word:list token} @@ -152,7 +152,7 @@ Module Defs(Import G:T). Fixpoint pt_size {head_symbol word sem} (tree:parse_tree head_symbol word sem) := - match tree with + match tree with | Terminal_pt _ _ => 1 | Non_terminal_pt _ _ _ l => S (ptl_size l) end |