From a9541e2ee557c04c4bc3476a36a87bc7fcdb06bb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 23 Jun 2020 12:49:46 +0200
Subject: Ensure statically that Hint Extern comes with a pattern.

---
 tactics/class_tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/class_tactics.ml')

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
-- 
cgit v1.2.3