Merge branch 'v8.5'

2 files changed, 21 insertions, 16 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c3968f8963..b8fb61e35d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1765,12 +1765,12 @@ let build_inversion_problem loc env sigma tms t =
       Pushed (true,((tm,tmtyp),deps,na)))
       dep_sign decls in
   let subst = List.map (fun (na,t) -> (na,lift n t)) subst in
-  (* [eqn1] is the first clause of the auxiliary pattern-matching that
+  (* [main_eqn] is the main clause of the auxiliary pattern-matching that
      serves as skeleton for the return type: [patl] is the
      substructure of constructors extracted from the list of
      constraints on the inductive types of the multiple terms matched
      in the original pattern-matching problem Xi *)
-  let eqn1 =
+  let main_eqn =
     { patterns = patl;
       alias_stack = [];
       eqn_loc = Loc.ghost;
@@ -1781,19 +1781,24 @@ let build_inversion_problem loc env sigma tms t =
               rhs_vars = List.map fst subst;
               avoid_ids = avoid;
 	      it = Some (lift n t) } } in
-  (* [eqn2] is the default clause of the auxiliary pattern-matching: it will
-     catch the clauses of the original pattern-matching problem Xi whose
-     type constraints are incompatible with the constraints on the
+  (* [catch_all] is a catch-all default clause of the auxiliary
+     pattern-matching, if needed: it will catch the clauses
+     of the original pattern-matching problem Xi whose type
+     constraints are incompatible with the constraints on the
      inductive types of the multiple terms matched in Xi *)
-  let eqn2 =
-    { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl;
-      alias_stack = [];
-      eqn_loc = Loc.ghost;
-      used = ref false;
-      rhs = { rhs_env = pb_env;
-              rhs_vars = [];
-	      avoid_ids = avoid0;
-	      it = None } } in
+  let catch_all_eqn =
+    if List.for_all (irrefutable env) patl then
+      (* No need for a catch all clause *)
+      []
+    else
+      [ { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl;
+          alias_stack = [];
+          eqn_loc = Loc.ghost;
+          used = ref false;
+          rhs = { rhs_env = pb_env;
+                  rhs_vars = [];
+	          avoid_ids = avoid0;
+	          it = None } } ] in
   (* [pb] is the auxiliary pattern-matching serving as skeleton for the
       return type of the original problem Xi *)
   (* let sigma, s = Evd.new_sort_variable sigma in *)
@@ -1810,7 +1815,7 @@ let build_inversion_problem loc env sigma tms t =
       pred      = (*ty *) mkSort s;
       tomatch   = sub_tms;
       history   = start_history n;
-      mat       = [eqn1;eqn2];
+      mat       = main_eqn :: catch_all_eqn;
       caseloc   = loc;
       casestyle = RegularStyle;
       typing_function = build_tycon loc env pb_env s subst} in
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 43062a0e8d..afd86420e9 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -310,7 +310,7 @@ and cbv_stack_value info env = function
     | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk)))
         when red_set (info_flags info) fIOTA && Projection.unfolded p ->
       let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in
-	cbv_stack_value info env (arg, stk)
+	cbv_stack_value info env (strip_appl arg stk)
 
     (* may be reduced later by application *)
     | (FIXP(fix,env,[||]), APP(appl,TOP)) -> FIXP(fix,env,appl)