diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2017-02-02 18:45:28 +0100 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2017-05-23 10:04:50 +0200 |
| commit | 321a42bf24490b08e12af5d8c2cf627e01a25aba (patch) | |
| tree | d3d07b7af62e9ddf216384ff4a76a7d1b9639de4 /proofs | |
| parent | a2d43679596d86033ac52c16ac137d8cf2a06412 (diff) | |
Fix bindings handling of setoid_rewrite.
This fixes the discrepancy between "rewrite H with (1 := x)"
and "setoid_rewrite H with (1 := x)".
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0a90e0dbd..beed9e36b 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -661,7 +661,8 @@ let evar_of_binder holes = function | NamedHyp s -> evar_with_name holes s | AnonHyp n -> try - let h = List.nth holes (pred n) in + let nondeps = List.filter (fun hole -> not hole.hole_deps) holes in + let h = List.nth nondeps (pred n) in h.hole_evar with e when CErrors.noncritical e -> errorlabstrm "" (str "No such binder.") |