From e7466e052473f1996f5ec1aa4036dbe94146b9bd Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 20 Sep 2001 23:13:13 +0000
Subject: Correction (double) bug de Generalize Dependent

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 11c82f518..11c37aa3b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -677,12 +677,11 @@ let generalize_dep c gl =
 	  -> id::tothin
       | _ -> tothin
   in
-  let cl' =
-    List.fold_left 
-      (fun c d -> mkNamedProd_or_LetIn d c) (pf_concl gl) to_quantify in
+  let cl' = List.fold_right mkNamedProd_or_LetIn to_quantify (pf_concl gl) in
   let cl'' = generalize_goal gl c cl' in
+  let args = instance_from_named_context to_quantify in
   tclTHEN
-    (apply_type cl'' (c::(List.map mkVar qhyps)))
+    (apply_type cl'' (c::args))
     (thin (List.rev tothin'))
     gl
     
-- 
cgit v1.2.3