diff options
| author | msozeau | 2008-09-07 19:02:30 +0000 |
|---|---|---|
| committer | msozeau | 2008-09-07 19:02:30 +0000 |
| commit | 68323044efbacaa62d755451a40e3e2ef94d5736 (patch) | |
| tree | 0485868ea674372fb6545f4321dfb6aaf4b9dfd4 | |
| parent | 135c872c4a507726a633cc4025d284933fbc6660 (diff) | |
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
| -rw-r--r-- | contrib/subtac/equations.ml4 | 6 |
1 files changed, 5 insertions, 1 deletions
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 |