diff options
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, |