aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/extraargs.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/extraargs.ml4')
-rw-r--r--tactics/extraargs.ml45
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