Merge branch 'v8.5'

3 files changed, 23 insertions, 9 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 47d92f5e0..a5a7ace22 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1077,7 +1077,7 @@ let rec ungeneralize n ng body =
         let p = prod_applist p [mkRel (n+List.length sign+ng)] in
         it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in
       mkCase (ci,p,c,Array.map2 (fun q c ->
-        let sign,b = decompose_lam_n_assum q c in
+        let sign,b = decompose_lam_n_decls q c in
         it_mkLambda_or_LetIn (ungeneralize (n+q) ng b) sign)
         ci.ci_cstr_ndecls brs)
   | App (f,args) ->
@@ -1102,7 +1102,8 @@ let rec is_dependent_generalization ng body =
   | Case (ci,p,c,brs) ->
       (* We traverse a split *)
       Array.exists2 (fun q c ->
-        let _,b = decompose_lam_n_assum q c in is_dependent_generalization ng b)
+        let _,b = decompose_lam_n_decls q c in
+        is_dependent_generalization ng b)
         ci.ci_cstr_ndecls brs
   | App (g,args) ->
       (* We traverse an inner generalization *)
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 121ab7488..3fa037ffd 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -267,8 +267,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
-	  let ctx_b2,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in
-	  let ctx_b2',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in
+	  let ctx_b2,b2 = decompose_lam_n_decls ci.ci_cstr_ndecls.(0) b2 in
+	  let ctx_b2',b2' = decompose_lam_n_decls ci.ci_cstr_ndecls.(1) b2' in
 	  let n = rel_context_length ctx_b2 in
           let n' = rel_context_length ctx_b2' in
 	  if noccur_between 1 n b2 && noccur_between 1 n' b2' then
@@ -413,12 +413,25 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
             mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
           let sub = (env, c1) :: subargs env lc in
           try_aux sub mk_ctx next
-  | Case (ci,hd,c1,lc) ->
+  | Case (ci,p,c,brs) ->
+      (* Warning: this assumes predicate and branches to be
+         in canonical form using let and fun of the signature *)
+      let nardecls = List.length ci.ci_pp_info.ind_tags in
+      let sign_p,p = decompose_lam_n_decls (nardecls + 1) p in
+      let env_p = Environ.push_rel_context sign_p env in
+      let brs = Array.map2 decompose_lam_n_decls ci.ci_cstr_ndecls brs in
+      let sign_brs = Array.map fst brs in
+      let f (sign,br) = (Environ.push_rel_context sign env, br) in
+      let sub_br = Array.map f brs in
       let next_mk_ctx = function
-      | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
+      | c :: p :: brs ->
+        let p = it_mkLambda_or_LetIn p sign_p in
+        let brs =
+          Array.map2 it_mkLambda_or_LetIn (Array.of_list brs) sign_brs in
+        mk_ctx (mkCase (ci,p,c,brs))
       | _ -> assert false
       in
-      let sub = (env, c1) :: (env, hd) :: subargs env lc in
+      let sub = (env, c) :: (env_p, p) :: Array.to_list sub_br in
       try_aux sub next_mk_ctx next
   | Fix (indx,(names,types,bodies)) ->
     let nb_fix = Array.length types in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a1213e72b..b5228094a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -302,7 +302,7 @@ and contract_branch isgoal e (cdn,can,mkpat,b) =
 let is_nondep_branch c l =
   try
     (* FIXME: do better using tags from l *)
-    let sign,ccl = decompose_lam_n_assum (List.length l) c in
+    let sign,ccl = decompose_lam_n_decls (List.length l) c in
     noccur_between 1 (rel_context_length sign) ccl
   with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *)
     false
@@ -513,7 +513,7 @@ let rec detype flags avoid env sigma t =
           id,l
         with Not_found ->
           Id.of_string ("X" ^ string_of_int (Evar.repr evk)), 
-          (Array.map_to_list (fun c -> (Id.of_string "A",c)) cl)
+          (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl)
       in
         GEvar (dl,id,
                List.map (on_snd (detype flags avoid env sigma)) l)