aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tactics/tactics.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d02fe86653..4654817035 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5008,7 +5008,7 @@ let tclABSTRACT ?(opaque=true) name_op tac =
let s, gk = if opaque
then name_op_to_name name_op (Proof Theorem) "_subproof"
else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
- abstract_subproof ~opaque:opaque s gk tac
+ abstract_subproof ~opaque s gk tac
let unify ?(state=full_transparent_state) x y =
Proofview.Goal.s_enter { s_enter = begin fun gl ->