diff options
Diffstat (limited to 'src/versions/native/structures.ml')
| -rw-r--r-- | src/versions/native/structures.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml index 28ad7e2..62907d1 100644 --- a/src/versions/native/structures.ml +++ b/src/versions/native/structures.ml @@ -70,3 +70,5 @@ let vernacentries_interp expr = let pr_constr_env = Printer.pr_constr_env let lift = Term.lift + +let mk_tactic t = t |