diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 09dcb49f4..de72f2b5c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1090,12 +1090,15 @@ and interp_ltac_reference loc' mustbetac ist gl = function and interp_tacarg ist gl arg = let evdref = ref (project gl) in let v = match arg with - | TacVoid -> in_gen (topwit wit_unit) () + | TacGeneric arg -> + let gl = { gl with sigma = !evdref } in + let (sigma, v) = Geninterp.generic_interp ist gl arg in + evdref := sigma; + v | Reference r -> let (sigma,v) = interp_ltac_reference dloc false ist gl r in evdref := sigma; v - | Integer n -> in_gen (topwit wit_int) n | IntroPattern ipat -> let ans = interp_intro_pattern ist gl ipat in in_gen (topwit wit_intro_pattern) ans |