From 4bfb3331804fd191a1d5fb92e99ae17b080f4f7b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 8 Apr 2014 15:59:36 +0200
Subject: Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.

---
 proofs/clenv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

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 }
-- 
cgit v1.2.3