From cd3040d5bb67bd17a3c4d20e3324d285657e215d Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 25 Jul 2018 17:10:43 +0200
Subject: [ssr] assertion -> error message (Fix #8134)

---
 plugins/ssr/ssripats.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 46fde41150..1dbacf0ff7 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -379,8 +379,9 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr =
          let ctx, last = EConstr.decompose_prod_assum sigma concl in
          let args = match EConstr.kind_of_type sigma last with
            | Term.AtomicType (hd, args) ->
-               assert(Ssrcommon.is_protect hd env sigma);
-               args
+               if Ssrcommon.is_protect hd env sigma then args
+               else Ssrcommon.errorstrm
+                  (Pp.str "Too many names in intro pattern")
            | _ -> assert false in
          let case = args.(Array.length args-1) in
          if not(EConstr.Vars.closed0 sigma case)
-- 
cgit v1.2.3