diff options
Diffstat (limited to 'src/tac2intern.ml')
| -rw-r--r-- | src/tac2intern.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/tac2intern.ml b/src/tac2intern.ml index 5d2fc2b47b..2b234d7aec 100644 --- a/src/tac2intern.ml +++ b/src/tac2intern.ml @@ -789,7 +789,11 @@ let rec intern_rec env = function let ist = empty_glob_sign genv in let ist = { ist with extra = Store.set ist.extra ltac2_env env } in let arg, tpe = Flags.with_option Ltac_plugin.Tacintern.strict_check (fun () -> obj.ml_intern self ist arg) () in - (GTacExt (tag, arg), tpe) + let e = match arg with + | GlbVal arg -> GTacExt (tag, arg) + | GlbTacexpr e -> e + in + (e, tpe) and intern_rec_with_constraint env e exp = let loc = loc_of_tacexpr e in |