From 7e6e533b148c9d57251388e9f1646a6829d10bfb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 19 Jan 2014 03:21:58 +0100
Subject: Fixing an interpretation bug with tactics in notations. For some
 obscure reason, Ltac interpretation does not allow tactics of the following
 shape : let x := bla in TacGeneric tac. Hence we force genargs to be tactics
 and build the resulting hole tactic from scratch.

---
 interp/constrintern.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5731d7d044..e765fa8cd6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -559,6 +559,11 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
       | Some arg ->
         let open Tacexpr in
         let open Genarg in
+        let wit = glbwit Constrarg.wit_tactic in
+        let body =
+          if has_type arg wit then out_gen wit arg
+          else assert false (** FIXME *)
+        in
         let mk_env id (c, (tmp_scope, subscopes)) accu =
           let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
           let gc = intern nenv c in
@@ -566,9 +571,8 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
           ((loc, id), c) :: accu
         in
         let bindings = Id.Map.fold mk_env terms [] in
-        let body = TacArg (loc, TacGeneric arg) in
         let tac = TacLetIn (false, bindings, body) in
-        let arg = in_gen (glbwit Constrarg.wit_tactic) tac in
+        let arg = in_gen wit tac in
         Some arg
       in
       GHole (loc, knd, arg)
-- 
cgit v1.2.3