diff options
| author | Pierre-Marie Pédrot | 2020-10-15 15:15:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-15 15:15:44 +0200 |
| commit | 476520ab32d3e975f6cee8aabcd04ad5fdfbbd77 (patch) | |
| tree | e8a75d0411c275635540f675449cc38b00c989fd /plugins/ltac/tacintern.ml | |
| parent | 4bf43453ec5f635ae87a2edeb4f51d95f2d5ac67 (diff) | |
| parent | 92ddd42345f9976a1e3b2cc2e53541ef0864ed0b (diff) | |
Merge PR #13098: Deprecating wit_var to the benefit of its synonymous wit_hyp
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Reviewed-by: ppedrot
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); |