diff options
| author | Hugo Herbelin | 2020-11-29 00:12:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-12-13 05:44:08 +0100 |
| commit | 79518ccb613d6a4a4bdec2bd67a8882df26144de (patch) | |
| tree | e25d6c59917e95be8dff25093b539c1abfd35f56 /tactics/tactics.ml | |
| parent | 1b43dfcb6facbc88c611db3ecb9076e377eebb34 (diff) | |
Removing unused internal introduction-patterns flag assert_style.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 88512b1fa0..528fa65d5a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2346,7 +2346,7 @@ let intro_or_and_pattern ?loc with_evars ll thin tac id = nv_with_let ll)) end -let rewrite_hyp_then assert_style with_evars thin l2r id tac = +let rewrite_hyp_then with_evars thin l2r id tac = let rew_on l2r = Hook.get forward_general_rewrite_clause l2r with_evars (mkVar id,NoBindings) in let subst_on l2r x rhs = @@ -2502,7 +2502,7 @@ let rec intro_patterns_core with_evars avoid ids thin destopt bound n tac = | IntroAction pat -> intro_then_gen (make_tmp_naming avoid l pat) destopt true false - (intro_pattern_action ?loc with_evars false pat thin destopt + (intro_pattern_action ?loc with_evars pat thin destopt (fun thin bound' -> intro_patterns_core with_evars avoid ids thin destopt bound' 0 (fun ids thin -> intro_patterns_core with_evars avoid ids thin destopt bound (n+1) tac l))) @@ -2526,7 +2526,7 @@ and intro_pattern_naming loc with_evars avoid ids pat thin destopt bound n tac l destopt true false (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l) -and intro_pattern_action ?loc with_evars style pat thin destopt tac id = +and intro_pattern_action ?loc with_evars pat thin destopt tac id = match pat with | IntroWildcard -> tac (CAst.(make ?loc id)::thin) None [] @@ -2535,7 +2535,7 @@ and intro_pattern_action ?loc with_evars style pat thin destopt tac id = | IntroInjection l' -> intro_decomp_eq ?loc l' thin tac id | IntroRewrite l2r -> - rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None []) + rewrite_hyp_then with_evars thin l2r id (fun thin -> tac thin None []) | IntroApplyOn ({CAst.loc=loc';v=f},{CAst.loc;v=pat}) -> let naming,tac_ipat = prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in @@ -2559,7 +2559,7 @@ and prepare_intros ?loc with_evars dft destopt = function intro_patterns_core with_evars Id.Set.empty [] thin destopt bound 0 (fun _ l -> clear_wildcards l) in fun id -> - intro_pattern_action ?loc with_evars true ipat [] destopt tac id) + intro_pattern_action ?loc with_evars ipat [] destopt tac id) | IntroForthcoming _ -> user_err ?loc (str "Introduction pattern for one hypothesis expected.") |