diff options
author | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
commit | e0d682ec25282a348d35c5b169abafec48555690 (patch) | |
tree | 1a46f0142a85df553388c932110793881f3af52f /plugins/subtac/subtac_command.ml | |
parent | 86535d84cc3cffeee1dcd8545343f234e7285530 (diff) |
Imported Upstream version 8.4dfsgupstream/8.4dfsg
Diffstat (limited to 'plugins/subtac/subtac_command.ml')
-rw-r--r-- | plugins/subtac/subtac_command.ml | 9 |
1 files changed, 8 insertions, 1 deletions
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, |