From 9cf6b3543bf369ccb4d3b0909ee3db96e074e24e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 10 Feb 2010 00:14:07 +0000
Subject: Fix [Existing Class] impl and add documentation. Fix computation of
 the dependency order of obligations that was not backwards-compatible.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12719 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/class_tactics.ml4 | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 5e9bb653c9..6463168985 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -261,13 +261,18 @@ type atac = auto_result tac
 
 let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
   let cty = Evarutil.nf_evar sigma cty in
-  let keep = not only_classes || 
-    let ctx, ar = decompose_prod cty in
+  let rec iscl env ty = 
+    let ctx, ar = decompose_prod_assum ty in
       match kind_of_term (fst (decompose_app ar)) with
       | Const c -> is_class (ConstRef c)
       | Ind i -> is_class (IndRef i)
-      | _ -> false
+      | _ -> 
+	  let env' = Environ.push_rel_context ctx env in
+	  let ty' = whd_betadeltaiota env' ar in
+	       if not (eq_constr ty' ar) then iscl env' ty'
+	       else false
   in
+  let keep = not only_classes || iscl env cty in
     if keep then let c = mkVar id in
       map_succeed 
 	(fun f -> try f (c,cty) with UserError _ -> failwith "") 
-- 
cgit v1.2.3