Extension of the recursive notations mechanism

- Added support for recursive notations with binders
- Added support for arbitrary large iterators in recursive notations
- More checks on the use of variables and improved error messages
- Do side-effects in metasyntax only when sure that everything is ok
- Documentation

Note: it seems there were a small bug in match_alist (instances obtained
from matching the first copy of iterator were not propagated).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 3 deletions

diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index d84a9d2eda..701c8f7079 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -120,7 +120,7 @@ type tomatch_stack = tomatch_status list
      originating from a subterm in which case real args are not dependent;
      it accounts for n+1 binders if dep or n binders if not dep
    - [PrProd] types abstracted term ([Abstract]); it accounts for one binder
-   - [PrCcl] types the right-hand-side
+   - [PrCcl] types the right-hand side
    - Aliases [Alias] have no trace in [predicate_signature]
 *)
 
@@ -1147,7 +1147,7 @@ let rec generalize_problem pb = function
 	  tomatch = Abstract d :: tomatch;
           pred = Option.map (generalize_predicate i d) pb'.pred }
 
-(* No more patterns: typing the right-hand-side of equations *)
+(* No more patterns: typing the right-hand side of equations *)
 let build_leaf pb =
   let rhs = extract_rhs pb in
   let tycon = match pb.pred with
@@ -1924,7 +1924,7 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
 
   let typing_fun tycon env = typing_fun tycon env isevars in
 
-  (* We build the matrix of patterns and right-hand-side *)
+  (* We build the matrix of patterns and right-hand side *)
   let matx = matx_of_eqns env eqns in
 
   (* We build the vector of terms to match consistently with the *)