From fc06cb87286e2b114c7f92500511d5914b8f7f48 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 22 Jul 2010 21:06:18 +0000
Subject: 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
---
 plugins/subtac/subtac_cases.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

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 *)
-- 
cgit v1.2.3