Merge branch 'v8.5'

9 files changed, 43 insertions, 25 deletions

diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index c421b4505b..e2bb2d1a00 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -78,9 +78,9 @@ val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_univer
 
 (** {6 Lookup functions for coercion paths } *)
 
-val lookup_path_between_class : cl_index * cl_index -> inheritance_path
-(** @raise Not_found when no such path exists *)
+(** @raise Not_found in the following functions when no path exists *)
 
+val lookup_path_between_class : cl_index * cl_index -> inheritance_path
 val lookup_path_between : env -> evar_map -> types * types ->
       types * types * inheritance_path
 val lookup_path_to_fun_from : env -> evar_map -> types ->
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6765ca130b..e61e52c178 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -345,7 +345,7 @@ let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
     ~filter:Typeclasses.no_goals ~split:false ~fail:false env evd
 
-(* appliquer le chemin de coercions p à hj *)
+(* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
 let apply_coercion env sigma p hj typ_cl =
   try
     let j,t,evd = 
@@ -367,7 +367,8 @@ let apply_coercion env sigma p hj typ_cl =
   with NoCoercion as e -> raise e
   | e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion")
 
-let inh_app_fun env evd j =
+(* Try to coerce to a funclass; raise NoCoercion if not possible *)
+let inh_app_fun_core env evd j =
   let t = whd_betadeltaiota env evd j.uj_type in
     match kind_of_term t with
     | Prod (_,_,_) -> (evd,j)
@@ -387,16 +388,17 @@ let inh_app_fun env evd j =
 	      (!evdref, res)
 	  with NoSubtacCoercion | NoCoercion ->
 	    (evd,j)
-          else (evd, j)
+          else raise NoCoercion
 
+(* Try to coerce to a funclass; returns [j] if no coercion is applicable *)
 let inh_app_fun resolve_tc env evd j =
-  try inh_app_fun env evd j
+  try inh_app_fun_core env evd j
   with
-  | Not_found when not resolve_tc 
+  | NoCoercion when not resolve_tc
     || not !use_typeclasses_for_conversion -> (evd, j)
-  | Not_found ->
-    try inh_app_fun env (saturate_evd env evd) j
-    with Not_found -> (evd, j)
+  | NoCoercion ->
+    try inh_app_fun_core env (saturate_evd env evd) j
+    with NoCoercion -> (evd, j)
 
 let inh_tosort_force loc env evd j =
   try
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 97b1b16455..bb07bf0563 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -552,13 +552,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 
     | MaybeFlexible v1, MaybeFlexible v2 -> begin
         match kind_of_term term1, kind_of_term term2 with
-        | LetIn (na,b1,t1,c'1), LetIn (_,b2,t2,c'2) ->
+        | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) ->
         let f1 i =
           ise_and i
 	    [(fun i -> evar_conv_x ts env i CONV b1 b2);
 	     (fun i ->
 	       let b = nf_evar i b1 in
 	       let t = nf_evar i t1 in
+               let na = Nameops.name_max na1 na2 in
 	       evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2);
 	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
 	and f2 i =
@@ -666,13 +667,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     end
 
     | Rigid, Rigid when isLambda term1 && isLambda term2 ->
-        let (na,c1,c'1) = destLambda term1 in
-        let (_,c2,c'2) = destLambda term2 in
+        let (na1,c1,c'1) = destLambda term1 in
+        let (na2,c2,c'2) = destLambda term2 in
         assert app_empty;
         ise_and evd
           [(fun i -> evar_conv_x ts env i CONV c1 c2);
            (fun i ->
 	     let c = nf_evar i c1 in
+             let na = Nameops.name_max na1 na2 in
 	     evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)]
 
     | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
@@ -726,12 +728,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
                UnifFailure (evd,UnifUnivInconsistency p)
 	     | e when Errors.noncritical e -> UnifFailure (evd,NotSameHead))
 
-	| Prod (n,c1,c'1), Prod (_,c2,c'2) when app_empty ->
+	| Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty ->
             ise_and evd
               [(fun i -> evar_conv_x ts env i CONV c1 c2);
                (fun i ->
  	         let c = nf_evar i c1 in
-	         evar_conv_x ts (push_rel (n,None,c) env) i pbty c'1 c'2)]
+                 let na = Nameops.name_max n1 n2 in
+	         evar_conv_x ts (push_rel (na,None,c) env) i pbty c'1 c'2)]
 
 	| Rel x1, Rel x2 ->
 	    if Int.equal x1 x2 then
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index bfd19c6c7d..ac1692f451 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -157,6 +157,7 @@ let restrict_evar_key evd evk filter candidates =
     end
 
 (* Restrict an applied evar and returns its restriction in the same context *)
+(* (the filter is assumed to be at least stronger than the original one) *)
 let restrict_applied_evar evd (evk,argsv) filter candidates =
   let evd,newevk = restrict_evar_key evd evk filter candidates in
   let newargsv = match filter with
@@ -693,7 +694,8 @@ let rec find_projectable_vars with_evars aliases sigma y subst =
     (* Then test if [idc] is (indirectly) bound in [subst] to some evar *)
     (* projectable on [y] *)
       if with_evars then
-        let idcl' = List.filter (fun (c,_,id) -> isEvar c) idcl in
+        let f (c,_,id) = isEvar c && is_undefined sigma (fst (destEvar c)) in
+        let idcl' = List.filter f idcl in
         match idcl' with
         | [c,_,id] ->
           begin
@@ -885,6 +887,9 @@ let filter_candidates evd evk filter candidates_update =
       else
         UpdateWith l'
 
+(* Given a filter refinement for the evar [evk], restrict it so that
+   dependencies are preserved *)
+
 let closure_of_filter evd evk = function
   | None -> None
   | Some filter ->
@@ -892,8 +897,11 @@ let closure_of_filter evd evk = function
   let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in
   let test b (id,c,_) = b || Idset.mem id vars || match c with None -> false | Some c -> not (isRel c || isVar c) in
   let newfilter = Filter.map_along test filter (evar_context evi) in
+  (* Now ensure that restriction is at least what is was originally *)
+  let newfilter = Option.cata (Filter.map_along (&&) newfilter) newfilter (Filter.repr (evar_filter evi)) in
   if Filter.equal newfilter (evar_filter evi) then None else Some newfilter
 
+(* The filter is assumed to be at least stronger than the original one *)
 let restrict_hyps evd evk filter candidates =
     (* What to do with dependencies?
        Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y.
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 90aa8000a8..cb091f2d6f 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -322,7 +322,8 @@ let instantiate_params t args sign =
 let get_constructor ((ind,u as indu),mib,mip,params) j =
   assert (j <= Array.length mip.mind_consnames);
   let typi = mis_nf_constructor_type (indu,mib,mip) j in
-  let typi = instantiate_params typi params mib.mind_params_ctxt in
+  let ctx = Vars.subst_instance_context u mib.mind_params_ctxt in
+  let typi = instantiate_params typi params ctx in
   let (args,ccl) = decompose_prod_assum typi in
   let (_,allargs) = decompose_app ccl in
   let vargs = List.skipn (List.length params) allargs in
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index b4b6b8aab8..2432b8d291 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -150,14 +150,12 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        begin match engagement env with
-        | Some ImpredicativeSet ->
+        if is_impredicative_set env then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
-        | _ ->
+        else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (sup u1 type0_univ)
-        end
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Pos,  Type u2)  -> Type (sup type0_univ u2)
     (* Product rule (Prop,Type_i,Type_i) *)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 6dc0d1f3c2..7fde7b7ac4 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -190,7 +190,7 @@ let cs_pattern_of_constr t =
 (* Intended to always succeed *)
 let compute_canonical_projections (con,ind) =
   let env = Global.env () in
-  let ctx = Environ.constant_context env con in
+  let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in
   let u = Univ.UContext.instance ctx in
   let v = (mkConstU (con,u)) in
   let ctx = Univ.ContextSet.of_context ctx in
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 743bc3b19b..fb55265526 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -126,9 +126,11 @@ let retype ?(polyprop=true) sigma =
     | App(f,args) ->
         strip_outer_cast
           (subst_type env sigma (type_of env f) (Array.to_list args))
-    | Proj (p,c) -> 
+    | Proj (p,c) ->
        let ty = type_of env c in
-       Inductiveops.type_of_projection_knowing_arg env sigma p c ty
+       (try
+	   Inductiveops.type_of_projection_knowing_arg env sigma p c ty
+	 with Invalid_argument _ -> retype_error BadRecursiveType)
     | Cast (c,_, t) -> t
     | Sort _ | Prod _ -> mkSort (sort_of env cstr)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b5fe5d0b6d..24e06007e9 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -676,7 +676,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	| Evar (evk,_ as ev), Evar (evk',_)
             when not (Evar.Set.mem evk flags.frozen_evars)
               && Evar.equal evk evk' ->
-	    sigma,metasubst,((curenv,ev,cN)::evarsubst)
+            let sigma',b = constr_cmp cv_pb sigma flags cM cN in
+            if b then
+	      sigma',metasubst,evarsubst
+            else
+	      sigma,metasubst,((curenv,ev,cN)::evarsubst)
 	| Evar (evk,_ as ev), _
             when not (Evar.Set.mem evk flags.frozen_evars) 
 	      && not (occur_evar evk cN) ->