Merge branch 'v8.5'

5 files changed, 43 insertions, 12 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7c3165fa8e..fcbe90b6a7 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -285,11 +285,13 @@ let inductive_template evdref env tmloc ind =
    applist (mkIndU indu,List.rev evarl)
 
 let try_find_ind env sigma typ realnames =
-  let (IndType(_,realargs) as ind) = find_rectype env sigma typ in
+  let (IndType(indf,realargs) as ind) = find_rectype env sigma typ in
   let names =
     match realnames with
       | Some names -> names
-      | None -> List.make (List.length realargs) Anonymous in
+      | None ->
+          let ind = fst (fst (dest_ind_family indf)) in
+          List.make (inductive_nrealdecls ind) Anonymous in
   IsInd (typ,ind,names)
 
 let inh_coerce_to_ind evdref env loc ty tyi =
@@ -730,7 +732,17 @@ let set_declaration_name x (_,c,t) = (x,c,t)
 
 let recover_initial_subpattern_names = List.map2 set_declaration_name
 
-let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t))
+let recover_and_adjust_alias_names names sign =
+  let rec aux = function
+  | [],[] ->
+      []
+  | x::names, (_,None,t)::sign ->
+      (x,(alias_of_pat x,None,t)) :: aux (names,sign)
+  | names, (na,(Some _ as c),t)::sign ->
+      (PatVar (Loc.ghost,na),(na,c,t)) :: aux (names,sign)
+  | _ -> assert false
+  in
+  List.split (aux (names,sign))
 
 let push_rels_eqn sign eqn =
   {eqn with
@@ -1695,11 +1707,12 @@ let build_inversion_problem loc env sigma tms t =
 	let pat,acc = make_patvar t acc in
 	let indf' = lift_inductive_family n indf in
 	let sign = make_arity_signature env true indf' in
-	let sign = recover_alias_names alias_of_pat (pat :: List.rev patl) sign in
-	let p = List.length realargs in
+        let patl = pat :: List.rev patl in
+	let patl,sign = recover_and_adjust_alias_names patl sign in
+	let p = List.length patl in
 	let env' = push_rel_context sign env in
-	let patl',acc_sign,acc = aux (n+p+1) env' (sign@acc_sign) tms acc in
-	patl@pat::patl',acc_sign,acc
+	let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in
+	List.rev_append patl patl',acc_sign,acc
     | (t, NotInd (bo,typ)) :: tms ->
       let pat,acc = make_patvar t acc in
       let d = (alias_of_pat pat,None,typ) in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index adf714db35..7f6a4a6442 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -273,7 +273,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let ind_tags =
-    rel_context_tags (List.firstn mip.mind_nrealargs mip.mind_arity_ctxt) in
+    rel_context_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in
   let cstr_tags =
     Array.map2 (fun c n ->
       let d,_ = decompose_prod_assum c in
@@ -526,7 +526,7 @@ let type_case_branches_with_names env indspec p c =
   let (params,realargs) = List.chop nparams args in
   let lbrty = Inductive.build_branches_type ind specif params p in
   (* Build case type *)
-  let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in
+  let conclty = Reduction.betazeta_appvect (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
   (* Adjust names *)
   if is_elim_predicate_explicitly_dependent env p (ind,params) then
     (set_pattern_names env (fst ind) lbrty, conclty)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index ec34383820..09eb38bd12 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -64,7 +64,10 @@ module ReductionBehaviour = struct
         if Lib.is_in_section (ConstRef c) then
           let vars, _, _ = Lib.section_segment_of_constant c in
           let extra = List.length vars in
-          let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in
+          let nargs' =
+             if b.b_nargs = max_int then max_int
+             else if b.b_nargs < 0 then b.b_nargs
+             else b.b_nargs + extra in
           let recargs' = List.map ((+) extra) b.b_recargs in
           { b with b_nargs = nargs'; b_recargs = recargs' }
         else b
@@ -1628,3 +1631,16 @@ let head_unfold_under_prod ts env _ c =
 	    | Const cst -> beta_applist (unfold cst,l)
 	    | _ -> c in
   aux c
+
+let betazetaevar_applist sigma n c l =
+  let rec stacklam n env t stack =
+    if Int.equal n 0 then applist (substl env t, stack) else
+    match kind_of_term t, stack with
+    | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
+    | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
+    | Evar ev, _ ->
+      (match safe_evar_value sigma ev with
+      | Some body -> stacklam n env body stack
+      | None -> applist (substl env t, stack))
+    | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+  stacklam n [] c l
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 7c61d4e143..d4f061c5be 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -278,6 +278,7 @@ val whd_meta : evar_map -> constr -> constr
 val plain_instance : constr Metamap.t -> constr -> constr
 val instance : evar_map -> constr Metamap.t -> constr -> constr
 val head_unfold_under_prod : transparent_state -> reduction_function
+val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
 
 (** {6 Heuristic for Conversion with Evar } *)
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index cd52ba44da..a56861c683 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -100,7 +100,7 @@ let retype ?(polyprop=true) sigma =
     | Ind ind -> rename_type_of_inductive env ind
     | Construct cstr -> rename_type_of_constructor env cstr
     | Case (_,p,c,lf) ->
-        let Inductiveops.IndType(_,realargs) =
+        let Inductiveops.IndType(indf,realargs) =
           let t = type_of env c in
           try Inductiveops.find_rectype env sigma t
           with Not_found ->
@@ -109,7 +109,8 @@ let retype ?(polyprop=true) sigma =
             Inductiveops.find_rectype env sigma t
           with Not_found -> retype_error BadRecursiveType
         in
-        let t = whd_beta sigma (applist (p, realargs)) in
+        let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in
+        let t = betazetaevar_applist sigma n p realargs in
         (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
           | Prod _ -> whd_beta sigma (applist (t, [c]))
           | _ -> t)