diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-27 12:19:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-27 12:19:24 +0000 |
| commit | 9a149e5af3e77dc176a5233ef6f1ab519a9d3bdb (patch) | |
| tree | 3f4d4241c26ecfccd5afe2ad9567aad2b018aace /library | |
| parent | 71f0f4a08b1f1fdace0e738a3a51d07193155fe4 (diff) | |
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
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/library/declare.ml b/library/declare.ml index b6da49320..3e561390e 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) |