diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-11 12:48:23 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-25 15:13:25 -0400 |
| commit | 1e046726dc9352f7979ebdeba0d750e44016fea5 (patch) | |
| tree | 9dcf13b4a09073cff1b97eda5f2a16327096ab8b /tactics | |
| parent | b348a11ccc4913598b72e4ecbb58811bcccd7bfc (diff) | |
transparent abstract: Respond to review comment
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8f791cdcf..d02fe8665 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4986,7 +4986,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = end } let abstract_subproof ~opaque id gk tac = - cache_term_by_tactic_then ~opaque:opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args))) + cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args))) let anon_id = Id.of_string "anonymous" |