[eacsl] Update grammars to stay in the frames

src/plugins/e-acsl/doc/refman/fn_behavior.tex

 \begin{syntax}
-  [ function-contract ] ::= requires-clause*
-                            { decreases-clause? } simple-clause*
-                            named-behavior* completeness-clause*
+  [ function-contract ] ::= requires-clause* ;
+                            { decreases-clause? } simple-clause* ;
+                            named-behavior* completeness-clause* ;
   \
   clause-kind ::= "check" | "admit"
   \
@@ -9,7 +9,7 @@
   \
   { decreases-clause } ::= { "decreases" term ("for" id)? ";" }
   \
-  [ simple-clause ] ::= { assigns-clause } | ensures-clause
+  [ simple-clause ] ::= { assigns-clause } | ensures-clause ;
                         | { allocation-clause} | { abrupt-clause }
   \
   { assigns-clause } ::= { "assigns" locations ";" }
@@ -26,6 +26,6 @@
   \
   assumes-clause ::= "assumes" pred ";"
   \
-  completeness-clause ::= "complete" "behaviors" (id (","id)*)? ";"
+  completeness-clause ::= "complete" "behaviors" (id (","id)*)? ";" ;
                         | "disjoint" "behaviors" (id (","id)*)? ";"
 \end{syntax}

src/plugins/e-acsl/doc/refman/model.tex

 \begin{syntax}
   declaration ::= C-declaration ;
-  | {"/*@" "model" parameter ";" "*/"} ; model variable
+  | {"/*@" "model" parameter ";" "*/"} ; \hspace{-7mm} model variable
   | { "/*@" "model" C-type-name "{" parameter ";"? "}" ";" "*/" } ; model field
 \end{syntax}

src/plugins/e-acsl/doc/refman/predicate.tex

@@ -2,31 +2,31 @@
   rel-op ::= "==" | "!=" | "<=" | ">=" | ">" | "<"
        \
   pred ::= "\true" | "\false" ;
-       | term (rel-op term)+ ; comparisons
-       | id "(" term ("," term)* ")" ; predicate application
-       | "(" pred ")" ; parentheses
-       | [ pred "&&" pred ] ; conjunction
-       | [ pred "||" pred ] ; disjunction
-       | [ pred "==>" pred ] ; implication
-       | pred "<==>" pred ; equivalence
-       | "!" pred ; negation
-       | [ { pred "^^" pred } ] ; exclusive or
-       | [ term "?" pred ":" pred ] ; ternary condition
+       | term (rel-op term)+ ;               \hspace{-10mm} comparisons
+       | id "(" term ("," term)* ")" ;       \hspace{-10mm} predicate application
+       | "(" pred ")" ;                      \hspace{-10mm} parentheses
+       | [ pred "&&" pred ] ;                \hspace{-10mm} conjunction
+       | [ pred "||" pred ] ;                \hspace{-10mm} disjunction
+       | [ pred "==>" pred ] ;               \hspace{-10mm} implication
+       | pred "<==>" pred ;                  \hspace{-10mm} equivalence
+       | "!" pred ;                          \hspace{-10mm} negation
+       | [ { pred "^^" pred } ] ;            \hspace{-10mm} exclusive or
+       | [ term "?" pred ":" pred ] ;        \hspace{-10mm} ternary condition
        | [ pred "?" pred ":" pred ];
-       | "\let" id "=" term ";" pred ; local binding
+       | "\let" id "=" term ";" pred ;       \hspace{-10mm} local binding
        | { "\let" id "=" pred ";" pred };
-       | [ "\forall" binders ";" ] ; 
-           [ integer-guards "==>" pred ]; univ. integer quantification
+       | [ "\forall" binders ";" ] ;
+           [ integer-guards "==>" pred ];    \hspace{-10mm} univ. integer quantification
        | [ "\exists" binders ";" ];
-           [ integer-guards "&&" pred ] ; exist. integer quantification
+           [ integer-guards "&&" pred ] ;    \hspace{-10mm} exist. integer quantification
        | [ { "\forall" binders ";" } ] ;
-         [ { iterator-guard "==>" pred } ]; univ. iterator quantification
+         [ { iterator-guard "==>" pred } ];  \hspace{-10mm} univ. iterator quantification
        | [ { "\exists" binders ";" } ];
-         [ { iterator-guard "&&" pred } ] ; exist. iterator quantification
-       | [ { "\forall" binders ";" pred } ]; univ. quantification
-       | [ { "\exists" binders ";" pred } ]; exist. quantification
-       | id ":" pred ; syntactic naming
-       | string ":" pred ; syntactic naming
+         [ { iterator-guard "&&" pred } ] ;  \hspace{-10mm} exist. iterator quantification
+       | [ { "\forall" binders ";" pred } ]; \hspace{-10mm} univ. quantification
+       | [ { "\exists" binders ";" pred } ]; \hspace{-10mm} exist. quantification
+       | id ":" pred ;                       \hspace{-10mm} syntactic naming
+       | string ":" pred ;                   \hspace{-10mm} syntactic naming
        \
   [ integer-guards ] ::= [ interv  ("&&" interv)* ]
        \