diff options
| author | Hugo Herbelin | 2017-06-17 17:57:33 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-06-18 06:44:43 +0200 |
| commit | 4f64c2fd8af07a46de744af55c4a27834513f446 (patch) | |
| tree | 25429beae6ca19ded3bc9b5861fc6a5a78fbcb82 /kernel/cbytecodes.mli | |
| parent | 1d3703be3ab41d016c776bb29d9f5eff0cdb401d (diff) | |
Addressing #5434 (ltac pattern-matching refusing to match anonymous variables).
Ltac pattern-matching was requiring dependent variables to be named.
This "natural" expectation is however not guaranteed by unification:
an evar can be dependent on an anonymous variable, resulting in
elaborated terms with dependent anonymous variables (see example in
file 5434.v).
This commit "fixes" the problem by not requiring that dependent
variables are named in ltac pattern-matching. Ltac pattern-matching
names itself these anonymous dependent variables, using the same
strategy as the printer (i.e. using "H" to display such
internally-anonymous dependent variables).
Diffstat (limited to 'kernel/cbytecodes.mli')
0 files changed, 0 insertions, 0 deletions