diff options
Diffstat (limited to 'tactics/extraargs.ml4')
-rw-r--r-- | tactics/extraargs.ml4 | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index f768e98e4..158cecfc7 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -288,12 +288,11 @@ let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause = Option.map (fun l -> List.map - (fun id -> ( ([],trad_id id) ,Tacexpr.InHyp)) + (fun id -> ( (all_occurrences_expr,trad_id id) ,Tacexpr.InHyp)) l ) hyps; - Tacexpr.onconcl=concl; - Tacexpr.concl_occs = []} + Tacexpr.concl_occs = if concl then all_occurrences_expr else no_occurrences_expr} let raw_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause snd |