diff options
| author | Gaëtan Gilbert | 2020-08-28 12:50:05 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-28 16:31:09 +0200 |
| commit | 40f8632178d8418f2492f9b19405621ac70ea671 (patch) | |
| tree | 842912ab1f17574dac8438c887c94c2cde34a40b /tactics | |
| parent | 911f33f0a0ff648082d329841388f59e8cecf231 (diff) | |
Make abstract compatible with mangle names
Fix #12928
Fix #3146
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 6b575d0807..f53dc2ed84 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -78,7 +78,10 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = | None -> Proofview.Goal.concl gl | Some ty -> ty in let concl = it_mkNamedProd_or_LetIn concl sign in - let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in + let solve_tac = tclCOMPLETE + (Tactics.intros_mustbe_force (List.rev_map NamedDecl.get_id sign) <*> + tac) + in let effs, sigma, lem, args, safe = !declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl in let solve = |