coq-community / autosubst

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
https://www.ps.uni-saarland.de/autosubst
MIT License
52 stars 14 forks source link

Adapt to Coq PR #17084: maximal implicit arguments now added to references in defined Ltac code #30

Open herbelin opened 1 year ago

herbelin commented 1 year ago

In anticipation of a uniformisation in coq/coq#17084 of how references with maximal implicit arguments are interpreted in Ltac code (*), this PR fixes the tactic has_var in Autosubst_Derive.v so that when None is returned, it returns it with its implicit argument rather than without.

This is a priori backwards compatible, so it can be merged as soon as now.

(*) Prior to coq/coq#17084, maximal implicit arguments are inserted in interactive mode but not in non-interactive mode.