From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 plugins/subtac/subtac_command.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'plugins/subtac/subtac_command.ml')

diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index ced390aa..14a09032 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -380,9 +380,16 @@ let rec unfold f b =
     | Some (x, b') -> x :: unfold f b'
     | None -> []
 
+
+let find_annot loc id ctx = 
+  try rel_index id ctx
+  with Not_found -> 
+  user_err_loc(loc,"",
+	       str "No parameter named " ++ Nameops.pr_id id ++ str".")
+
 let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
   match n with
-  | Some (loc, n) -> [rel_index n fixctx]
+  | Some (loc, id) -> [find_annot loc id fixctx]
   | None ->
       (* If recursive argument was not given by user, we try all args.
 	 An earlier approach was to look only for inductive arguments,
-- 
cgit v1.2.3