Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.

1 files changed, 1 insertions, 1 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index afc8d3b70d..33df4ca978 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -121,7 +121,7 @@ let clenv_environments evd bound t =
 let mk_clenv_from_env environ sigma n (c,cty) =
   let evd = create_goal_evar_defs sigma in
   let (evd,args,concl) = clenv_environments evd n cty in
-  { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
+  { templval = mk_freelisted (applist (c,args));
     templtyp = mk_freelisted concl;
     evd = evd;
     env = environ }