diff options
Diffstat (limited to 'tactics/extraargs.ml4')
| -rw-r--r-- | tactics/extraargs.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 4a6c2ffb2..48d4afbc1 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -221,7 +221,7 @@ END let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause = {Tacexpr.onhyps= - Util.option_map + Option.map (fun l -> List.map (fun id -> ( ([],trad_id id) ,Tacexpr.InHyp)) |