From 455d5ee36dc36cbf094ddccf43059cddceedcd1f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 22 Dec 2013 02:32:49 +0100
Subject: Notations now accept the $(...)$ tactic-in-term syntax. They are
 resolved at internalization time.

---
 tactics/tacinterp.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b697d3635c..712191a736 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1185,6 +1185,9 @@ and tactic_of_value ist vle =
       let tac = eval_tactic ist t in
       catch_error_tac trace tac
   | (VFun _|VRec _) -> Proofview.tclZERO (UserError ("" , str "A fully applied tactic is expected."))
+  else if has_type vle (topwit wit_tactic) then
+    let tac = out_gen (topwit wit_tactic) vle in
+    eval_tactic ist tac
   else Proofview.tclZERO (UserError ("" , str"Expression does not evaluate to a tactic."))
 
 and eval_value ist tac =
-- 
cgit v1.2.3