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

1 files changed, 8 insertions, 3 deletions

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 "")