aboutsummaryrefslogtreecommitdiff
path: root/tactics/class_tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/class_tactics.ml')
-rw-r--r--tactics/class_tactics.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 36544883aa..378a3e718b 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -359,7 +359,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
Tacticals.New.tclTHEN fst snd
| Unfold_nth c ->
Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c])
- | Extern tacast -> conclPattern concl p tacast
+ | Extern (p, tacast) -> conclPattern concl p tacast
in
let tac = FullHint.run h tac in
let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in