Monomorphization (proof)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16002 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 2 deletions

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index c16e02b3f..aa3d13f8a 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -71,8 +71,8 @@ let map_strategy f l =
           match f q with
               Some q' -> q' :: ql
             | None -> ql) ql [] in
-      if ql'=[] then str else (lev,ql')::str) l [] in
-  if l'=[] then None else Some (false,l')
+      if List.is_empty ql' then str else (lev,ql')::str) l [] in
+  if List.is_empty l' then None else Some (false,l')
 
 let classify_strategy (local,_ as obj) =
   if local then Dispose else Substitute obj