From 6d684ec32bc62ff1e9528081a2369852cc5b5c65 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 6 Nov 2009 22:41:38 +0000
Subject: - Fix discharge bug in typeclasses: some constrs were not actually
 discharged on the other definitions in the section. - Avoid universe problem
 in generalize_eqs were we could give an [@eq_refl Set x x] proof where an
 [@eq Type x x] was expected.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12478 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b9d2d9cfef..97006c9e91 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2291,6 +2291,7 @@ let abstract_args gl generalize_vars dep id =
 	      List.hd rel, c
 	  in
 	  let argty = pf_type_of gl arg in
+	  let argty = if isSort argty then new_Type () else argty in
 	  let liftargty = lift (List.length ctx) argty in
 	  let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in
 	    match kind_of_term arg with
-- 
cgit v1.2.3