From 84140c29194446cc62f0024ea916cb530c329e46 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 27 Feb 2004 14:34:06 +0000
Subject: Erreur de Bruijn et oubli substitution alias dans annotation du
 'match'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5391 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1a2b3aa806..d80bacbfbe 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1029,8 +1029,13 @@ let generalize_predicate c ny d = function
       anomaly "generalize_predicate: expects a non trivial pattern"
 
 let rec extract_predicate l = function
-  | pred, Alias _::tms -> extract_predicate l (pred,tms)
+  | pred, Alias (deppat,nondeppat,_,_)::tms ->
+      let tms' = match kind_of_term nondeppat with
+        | Rel i -> replace_tomatch i deppat tms
+        | _ -> (* initial terms are not dependent *) tms in
+      extract_predicate l (pred,tms')
   | PrProd pred, Abstract d'::tms ->
+      let d' = map_rel_declaration (lift (List.length l)) d' in
       substl l (mkProd_or_LetIn d' (extract_predicate [] (pred,tms)))
   | PrLetIn ((0,dep),pred), Pushed ((cur,_),_)::tms ->
       extract_predicate (if dep then cur::l else l) (pred,tms)
-- 
cgit v1.2.3