diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 48 |
1 files changed, 41 insertions, 7 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0a8b5d01..0a4c0fbe 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id: tactics.ml 12956 2010-04-20 08:49:15Z herbelin $ *) open Pp open Util @@ -249,14 +249,51 @@ let change_option occl t = function Some id -> change_in_hyp occl t id | None -> change_in_concl occl t -let change occl c cls = +let out_arg = function + | ArgVar _ -> anomaly "Unevaluated or_var variable" + | ArgArg x -> x + +let adjust_clause occl cls = + (* warn as much as possible on loss of occurrence information *) (match cls, occl with ({onhyps=(Some(_::_::_)|None)} |{onhyps=Some(_::_);concl_occs=((false,_)|(true,_::_))}), Some _ -> error "No occurrences expected when changing several hypotheses." | _ -> ()); - onClauses (change_option occl c) cls + (* get at clause from cls if only goal or one hyp specified *) + let occl,cls = match occl with + | None -> None,cls + | Some (occs,c) -> + if cls.onhyps=Some[] && occs=all_occurrences then + Some (on_snd (List.map out_arg) cls.concl_occs,c), + {cls with concl_occs=all_occurrences_expr} + else + match cls.onhyps with + | Some[(occs',id),l] when + cls.concl_occs=no_occurrences_expr && occs=all_occurrences -> + Some (on_snd (List.map out_arg) occs',c), + {cls with onhyps=Some[(all_occurrences_expr,id),l]} + | _ -> + occl,cls in + (* check if cls has still specified occs *) + if cls.onhyps <> None && + List.exists (fun ((occs,_),_) -> occs <> all_occurrences_expr) + (Option.get cls.onhyps) + || cls.concl_occs <> all_occurrences_expr && + cls.concl_occs <> no_occurrences_expr + then + Flags.if_verbose Pp.msg_warning + (if cls.onhyps=Some[] then + str "Trailing \"at\" modifier not taken into account." + else + str "\"at\" modifier in clause \"in\" not taken into account."); + (* Anticipate on onClauses which removes concl if not at all occs *) + if cls.concl_occs=no_occurrences_expr then cls + else {cls with concl_occs=all_occurrences_expr} + +let change occl c cls = + onClauses (change_option occl c) (adjust_clause occl cls) (* Pour usage interne (le niveau User est pris en compte par reduce) *) let red_in_concl = reduct_in_concl (red_product,DEFAULTcast) @@ -1397,10 +1434,6 @@ let quantify lconstr = the left of each x1, ...). *) -let out_arg = function - | ArgVar _ -> anomaly "Unevaluated or_var variable" - | ArgArg x -> x - let occurrences_of_hyp id cls = let rec hyp_occ = function [] -> None @@ -2546,6 +2579,7 @@ let induction_tac_felim with_evars indvars scheme gl = let apply_induction_in_context isrec hyp0 indsign indvars names induct_tac gl = let env = pf_env gl in let statlists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in + let deps = List.map (fun (id,c,t)-> (id,c,refresh_universes_strict t)) deps in let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in let names = compute_induction_names (Array.length indsign) names in let dephyps = List.map (fun (id,_,_) -> id) deps in |