diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-24 23:27:14 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-24 23:27:14 +0200 |
commit | 860dc1cb91549068cf65f963bf819f47eb13ebe4 (patch) | |
tree | 419adf42d07f3bcc2f979eb1f42fa3cd1fd7c585 /pretyping/evarsolve.ml | |
parent | 12c78d4e45ccc9b923cd300f981ef205fee1c650 (diff) | |
parent | 8232f27773f3463600fbaac0f70966bd4893ea20 (diff) |
Merge branch '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 6e5ded152..bafb009f5 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) |