diff options
| author | Pierre-Marie Pédrot | 2014-01-19 03:21:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-01-19 03:21:58 +0100 |
| commit | 7e6e533b148c9d57251388e9f1646a6829d10bfb (patch) | |
| tree | f1b4f7e9c0f90128ddb8b7ccc218d0a784bd5e05 | |
| parent | 029854c7f0c10caf0c26b1e3d73ae011c54ac80e (diff) | |
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.
| -rw-r--r-- | interp/constrintern.ml | 8 |
1 files 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) |