From 0d33024ff79c38d52fde49e23d0e45d9c22eefbe Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 12 Sep 2020 20:54:22 -0700
Subject: Convert 2nd part of rewriting chapter to prodn

---
 tactics/redexpr.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index 87cae3abe5..3ee85f6b1b 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -271,11 +271,14 @@ let reduction_of_red_expr env r =
 let error_illegal_clause () =
   CErrors.user_err Pp.(str "\"at\" clause not supported in presence of an occurrence clause.")
 
+let error_multiple_patterns () =
+  CErrors.user_err Pp.(str "\"at\" clause in occurences not supported with multiple patterns or references.")
+
 let error_illegal_non_atomic_clause () =
   CErrors.user_err Pp.(str "\"at\" clause not supported in presence of a non atomic \"in\" clause.")
 
-let error_occurrences_not_unsupported () =
-  CErrors.user_err Pp.(str "Occurrences not supported for this reduction tactic.")
+let error_at_in_occurrences_not_supported () =
+  CErrors.user_err Pp.(str "\"at\" clause not supported for this reduction tactic.")
 
 let bind_red_expr_occurrences occs nbcl redexp =
   let open Locus in
@@ -292,14 +295,14 @@ let bind_red_expr_occurrences occs nbcl redexp =
   else
     match redexp with
     | Unfold (_::_::_) ->
-        error_illegal_clause ()
+        error_multiple_patterns ()
     | Unfold [(occl,c)] ->
         if occl != AllOccurrences then
           error_illegal_clause ()
         else
           Unfold [(occs,c)]
     | Pattern (_::_::_) ->
-        error_illegal_clause ()
+        error_multiple_patterns ()
     | Pattern [(occl,c)] ->
         if occl != AllOccurrences then
           error_illegal_clause ()
@@ -322,7 +325,7 @@ let bind_red_expr_occurrences occs nbcl redexp =
           CbvNative (Some (occs,c))
     | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _
     | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None ->
-        error_occurrences_not_unsupported ()
+        error_at_in_occurrences_not_supported ()
     | Unfold [] | Pattern [] ->
         assert false
 
-- 
cgit v1.2.3