From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:27:01 +0200 Subject: Imported Upstream version 8.4dfsg --- plugins/subtac/eterm.mli | 2 +- plugins/subtac/g_subtac.ml4 | 2 +- plugins/subtac/subtac.ml | 2 +- plugins/subtac/subtac_cases.ml | 2 +- plugins/subtac/subtac_cases.mli | 2 +- plugins/subtac/subtac_classes.ml | 2 +- plugins/subtac/subtac_classes.mli | 2 +- plugins/subtac/subtac_coercion.ml | 2 +- plugins/subtac/subtac_command.ml | 9 ++++++++- plugins/subtac/subtac_pretyping.ml | 2 +- plugins/subtac/subtac_pretyping_F.ml | 2 +- 11 files changed, 18 insertions(+), 11 deletions(-) (limited to 'plugins/subtac') diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli index 03d76f29..a0b693de 100644 --- a/plugins/subtac/eterm.mli +++ b/plugins/subtac/eterm.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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, diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index e56fa4f5..fac6b567 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*