aboutsummaryrefslogtreecommitdiff
path: root/user-contrib
diff options
context:
space:
mode:
authorJim Fehrle2020-10-11 19:15:51 -0700
committerJim Fehrle2020-10-27 12:17:21 -0700
commitede77b72328c98995c0636656bb71ba87861ddfe (patch)
tree69510ffd33c71a461b22dea76d42656bf4d3293d /user-contrib
parentb402adc12c00ba72046423d3a1737ccad517f70e (diff)
Rename tactic_expr -> ltac_expr
Diffstat (limited to 'user-contrib')
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg2
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 2da5344496..cc2cdf7ef8 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -80,7 +80,7 @@ let tac2def_syn = Entry.create "tac2def_syn"
let tac2def_mut = Entry.create "tac2def_mut"
let tac2mode = Entry.create "ltac2_command"
-let ltac1_expr = Pltac.tactic_expr
+let ltac1_expr = Pltac.ltac_expr
let tac2expr_in_env = Tac2entries.Pltac.tac2expr_in_env
let inj_wit wit loc x = CAst.make ~loc @@ CTacExt (wit, x)