diff options
| author | Jim Fehrle | 2020-10-11 19:15:51 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-27 12:17:21 -0700 |
| commit | ede77b72328c98995c0636656bb71ba87861ddfe (patch) | |
| tree | 69510ffd33c71a461b22dea76d42656bf4d3293d /plugins/ltac/pltac.ml | |
| parent | b402adc12c00ba72046423d3a1737ccad517f70e (diff) | |
Rename tactic_expr -> ltac_expr
Diffstat (limited to 'plugins/ltac/pltac.ml')
| -rw-r--r-- | plugins/ltac/pltac.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index b7b54143df..1631215d58 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -38,7 +38,8 @@ let clause_dft_concl = (* Main entries for ltac *) let tactic_arg = Entry.create "tactic_arg" -let tactic_expr = Entry.create "tactic_expr" +let ltac_expr = Entry.create "ltac_expr" +let tactic_expr = ltac_expr let binder_tactic = Entry.create "binder_tactic" let tactic = Entry.create "tactic" |