From 1e046726dc9352f7979ebdeba0d750e44016fea5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Apr 2017 12:48:23 -0400 Subject: transparent abstract: Respond to review comment https://github.com/coq/coq/pull/201#discussion_r110952601 --- tactics/tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') 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" -- cgit v1.2.3