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

1 files changed, 6 insertions, 1 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1a2b3aa80..d80bacbfb 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)