diff options
author | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2015-11-04 03:04:21 +0100 |
---|---|---|
committer | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2015-11-04 03:04:21 +0100 |
commit | 5664fddcab15ef4482d583673c75e07bd1e96d0a (patch) | |
tree | 878b22860e69405ba5cf6fd2798731dac8ce660c /cparser/validator/Grammar.v | |
parent | b960c83725d7e185ac5c6e3c0d6043c7dcd2f556 (diff) | |
parent | fe73ed58ef80da7c53c124302a608948fb190229 (diff) | |
download | compcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.tar.gz compcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.zip |
Merge remote-tracking branch 'origin/master' into parser_fix
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 |