From 9a149e5af3e77dc176a5233ef6f1ab519a9d3bdb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Nov 2000 12:19:24 +0000
Subject: Bug dans find_common_hyps_then_abstract en présence de défs locales

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@987 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/library/declare.ml b/library/declare.ml
index b6da493208..3e561390ef 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -314,11 +314,15 @@ let find_common_hyps_then_abstract c env hyps' hyps =
 	 (env,c))
 *)
 
+let rec quantify_extra_hyps c = function
+  | (id,None,t)::hyps -> mkNamedLambda id t (quantify_extra_hyps c hyps)
+  | (_,Some _,_)::hyps -> quantify_extra_hyps c hyps
+  | [] -> c
+
 let rec find_common_hyps_then_abstract c env hyps' = function
   | (id,_,_ as d) :: hyps when occur_decl env d hyps' ->
       find_common_hyps_then_abstract c (Environ.push_named_decl d env) hyps' hyps
-  | hyps ->
-      Environ.it_mkNamedLambda_or_LetIn c (List.rev hyps)
+  | hyps -> quantify_extra_hyps c hyps
 
 let find_common_hyps_then_abstract c env hyps' hyps =
   find_common_hyps_then_abstract c env hyps' (List.rev hyps)
-- 
cgit v1.2.3