From da88175778d6055d1ecf40c8f429cf855a4304cb Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 14 Apr 2014 17:20:22 +0200
Subject: Avoid u+k <= v constraints, don't take the sup of an algebraic
 universe during minimization.

---
 tactics/tactics.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0fbb511a7d..2db58978d1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -435,7 +435,8 @@ let id_of_name_with_default id = function
 let hid = Id.of_string "H"
 let xid = Id.of_string "X"
 
-let default_id_of_sort = function Prop _ -> hid | Type _ -> xid
+let default_id_of_sort s =
+  if Sorts.is_small s then hid else xid
 
 let default_id env sigma = function
   | (name,None,t) ->
-- 
cgit v1.2.3