From 68323044efbacaa62d755451a40e3e2ef94d5736 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 7 Sep 2008 19:02:30 +0000
Subject: Check [Equations] patterns are for the right function.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11385 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/subtac/equations.ml4 | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4
index f3f0e052bf..d17fbbf257 100644
--- a/contrib/subtac/equations.ml4
+++ b/contrib/subtac/equations.ml4
@@ -721,7 +721,11 @@ let interp_pats i isevar env impls pat sign recu =
     let patenv = match recu with None -> env' | Some ty -> push_named (i, None, ty) env' in
     let patt, _ = interp_constr_evars_impls ~evdref:isevar patenv ~impls:([],[]) pat in
       match kind_of_term patt with
-      | App (m, args) -> Array.to_list args
+      | App (m, args) -> 
+	  if not (eq_constr m (mkRel (succ (length varsctx)))) then
+	    user_err_loc (constr_loc pat, "interp_pats",
+			 str "Expecting a pattern for " ++ pr_id i)
+	  else Array.to_list args
       | _ -> user_err_loc (constr_loc pat, "interp_pats",
 			  str "Error parsing pattern: unnexpected left-hand side")
   in
-- 
cgit v1.2.3