diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/autorewrite.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 15 | ||||
| -rw-r--r-- | tactics/ppred.ml | 1 |
3 files changed, 10 insertions, 8 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index f824552705..3b8232d20a 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -145,7 +145,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = let try_do_hyps treat_id l = autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas in - if cl.concl_occs != AllOccurrences && + if not (Locusops.is_all_occurrences cl.concl_occs) && cl.concl_occs != NoOccurrences then Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.") diff --git a/tactics/equality.ml b/tactics/equality.ml index 769e702da1..a8cfc87f9c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -437,7 +437,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac) let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac ((c,l) : constr with_bindings) with_evars = - if occs != AllOccurrences then ( + if not (Locusops.is_all_occurrences occs) then ( rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac) else Proofview.Goal.enter begin fun gl -> @@ -595,15 +595,16 @@ let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () else check_required_library ["Coq";"Setoids";"Setoid"] -let check_setoid cl = +let check_setoid cl = + let concloccs = Locusops.occurrences_map (fun x -> x) cl.concl_occs in Option.fold_left - ( List.fold_left + (List.fold_left (fun b ((occ,_),_) -> - b||(Locusops.occurrences_map (fun x -> x) occ <> AllOccurrences) + b||(not (Locusops.is_all_occurrences (Locusops.occurrences_map (fun x -> x) occ))) ) ) - ((Locusops.occurrences_map (fun x -> x) cl.concl_occs <> AllOccurrences) && - (Locusops.occurrences_map (fun x -> x) cl.concl_occs <> NoOccurrences)) + (not (Locusops.is_all_occurrences concloccs) && + (concloccs <> NoOccurrences)) cl.onhyps let replace_core clause l2r eq = @@ -1724,7 +1725,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = tclTHENLIST ((if need_rewrite then [revert (List.map snd dephyps); - general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp); + general_rewrite dir AtLeastOneOccurrence true dep_proof_ok (mkVar hyp); (tclMAP (fun (dest,id) -> intro_move (Some id) dest) dephyps)] else [Proofview.tclUNIT ()]) @ diff --git a/tactics/ppred.ml b/tactics/ppred.ml index dd1bcd4699..d832dc279c 100644 --- a/tactics/ppred.ml +++ b/tactics/ppred.ml @@ -6,6 +6,7 @@ open Pputils let pr_with_occurrences pr keyword (occs,c) = match occs with + | AtLeastOneOccurrence -> hov 1 (pr c ++ spc () ++ keyword "at" ++ str" +") | AllOccurrences -> pr c | NoOccurrences -> |