diff options
| author | Hugo Herbelin | 2020-09-27 07:35:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-14 12:23:59 +0200 |
| commit | 92ddd42345f9976a1e3b2cc2e53541ef0864ed0b (patch) | |
| tree | 5136a7f5ef77bbc38a2a7f25c1b7684f3cd59354 /plugins/ltac/tacintern.ml | |
| parent | 411025844a4c005ce03d77c6c640807c28269d4a (diff) | |
Deprecating wit_var to the benefit of its synonymous wit_hyp.
Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
Diffstat (limited to 'plugins/ltac/tacintern.ml')
| -rw-r--r-- | plugins/ltac/tacintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index dea216045e..9c3b05fdf1 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -835,7 +835,7 @@ let () = Genintern.register_intern0 wit_ref (lift intern_global_reference); Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c)); Genintern.register_intern0 wit_ident intern_ident'; - Genintern.register_intern0 wit_var (lift intern_hyp); + Genintern.register_intern0 wit_hyp (lift intern_hyp); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); Genintern.register_intern0 wit_ltac (lift intern_ltac); Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis); |