From 0fec4583628dfba57c4bbcf10e8c1fc053c5ec93 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 4 Aug 2009 12:37:05 +0000 Subject: - Add more precise error localisation when one of the application fails in a chain of apply or apply-in. - Improved comments on the notions of permutation used in the library (still the equality relation in file Permutation.v misses the property of being effectively an equivalence relation, hence missing expected properties of this notion of permutation). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12261 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tactics.ml | 24 ++++++++++++++---------- 1 file changed, 14 insertions(+), 10 deletions(-) (limited to 'tactics/tactics.ml') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0224da6c8..ca64a8d3d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -840,7 +840,7 @@ let check_evars sigma evm gl = errorlabstrm "apply" (str"Uninstantiated existential variables: " ++ fnl () ++ pr_evar_defs rest) -let general_apply with_delta with_destruct with_evars (c,lbind) gl0 = +let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = let flags = if with_delta then default_unify_flags else default_no_delta_unify_flags in (* The actual type of the theorem. It will be matched against the @@ -874,9 +874,9 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl0 = with PretypeError _|RefinerError _|UserError _|Failure _|Exit -> if with_destruct then descend_in_conjunctions with_evars - try_main_apply (fun _ -> raise exn) c gl + try_main_apply (fun _ -> Stdpp.raise_with_loc loc exn) c gl else - raise exn + Stdpp.raise_with_loc loc exn in try_red_apply thm_ty0 in if evm = Evd.empty then try_main_apply with_destruct c gl0 @@ -888,19 +888,18 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl0 = let rec apply_with_ebindings_gen b e = function | [] -> tclIDTAC - | [cb] -> - general_apply b b e cb + | [cb] -> general_apply b b e cb | cb::cbl -> tclTHENLAST (general_apply b b e cb) (apply_with_ebindings_gen b e cbl) -let apply_with_ebindings cb = apply_with_ebindings_gen false false [cb] -let eapply_with_ebindings cb = apply_with_ebindings_gen false true [cb] +let apply_with_ebindings cb = apply_with_ebindings_gen false false [dloc,cb] +let eapply_with_ebindings cb = apply_with_ebindings_gen false true [dloc,cb] let apply_with_bindings (c,bl) = apply_with_ebindings (inj_open c,inj_ebindings bl) let eapply_with_bindings (c,bl) = - apply_with_ebindings_gen false true [inj_open c,inj_ebindings bl] + apply_with_ebindings_gen false true [dloc,(inj_open c,inj_ebindings bl)] let apply c = apply_with_ebindings (inj_open c,NoBindings) @@ -947,7 +946,8 @@ let apply_in_once_main flags innerclause (d,lbind) gl = with NotExtensibleClause -> raise err in aux (make_clenv_binding gl (d,thm) lbind) -let apply_in_once with_delta with_destruct with_evars id ((sigma,d),lbind) gl0 = +let apply_in_once with_delta with_destruct with_evars id + (loc,((sigma,d),lbind)) gl0 = let flags = if with_delta then default_unify_flags else default_no_delta_unify_flags in let t' = pf_get_hyp_typ gl0 id in @@ -1141,7 +1141,8 @@ let constructor_tac with_evars expctdnumopt i lbind gl = Array.length (snd (Global.lookup_inductive mind)).mind_consnames in check_number_of_constructors expctdnumopt i nconstr; let cons = mkConstruct (ith_constructor_of_inductive mind i) in - let apply_tac = general_apply true false with_evars (inj_open cons,lbind) in + let apply_tac = + general_apply true false with_evars (dloc,(inj_open cons,lbind)) in (tclTHENLIST [convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl @@ -1374,6 +1375,9 @@ let general_apply_in with_delta with_destruct with_evars id lemmas ipat gl = let apply_in simple with_evars = general_apply_in simple simple with_evars +let simple_apply_in id c = + apply_in false false id [dloc,((Evd.empty,c),NoBindings)] None + (**************************) (* Generalize tactics *) (**************************) -- cgit v1.2.3