diff options
| author | Matthieu Sozeau | 2016-10-21 18:16:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-10-21 18:16:16 +0200 |
| commit | 517cc63a18d95c02c2d2490adb110ff712d30375 (patch) | |
| tree | 22c6e527663803ceec47afc625bb1a2e5b75adad /pretyping/evarsolve.ml | |
| parent | cef86ed6f78e2efa703bd8772a43fbeba597bbe3 (diff) | |
| parent | 5609da1e08f950fab85b87b257ed343b491f1ef5 (diff) | |
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index d695d4537b..f1526faccc 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1599,8 +1599,6 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = * ass. *) -(* This criterion relies on the fact that we postpone only problems of the form: -?x [?x1 ... ?xn] = t or the symmetric case. *) let status_changed lev (pbty,_,t1,t2) = (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false) |