diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-25 12:55:43 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-25 12:55:43 +0200 |
| commit | 90fa7d931f45673df93d57f77e74af51a180db9d (patch) | |
| tree | d3d07b7af62e9ddf216384ff4a76a7d1b9639de4 | |
| parent | a2d43679596d86033ac52c16ac137d8cf2a06412 (diff) | |
| parent | 321a42bf24490b08e12af5d8c2cf627e01a25aba (diff) | |
Merge PR#416: Fix the way setoid_rewrite handles bindings.
| -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.") |