Merge remote branch 'upstream/master' into clean

Conflicts:
	Makefile.extr

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