Merge branch 'v8.5' into trunk

3 files changed, 15 insertions, 4 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e3dba232b2..0cadffa4fe 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -82,7 +82,7 @@ let search_guard loc env possible_indexes fixdefs =
        iraise (e, info));
     indexes
   else
-    (* we now search recursively amoungst all combinations *)
+    (* we now search recursively among all combinations *)
     (try
        List.iter
 	 (fun l ->
@@ -220,7 +220,7 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
   let c = if flags.expand_evars then nf_evar sigma c else c in
   sigma,c
 
-(* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 let allow_anonymous_refs = ref false
 
 (* Utilisé pour inférer le prédicat des Cases *)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7d1e0c9b5b..142b54513e 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -63,7 +63,7 @@ val all_no_fail_flags : inference_flags
 
 val all_and_fail_flags : inference_flags
 
-(** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+(** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 val allow_anonymous_refs : bool ref
   
 (** Generic call to the interpreter from glob_constr to open_constr, leaving
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 203b1ec8a6..01e1154e58 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -673,6 +673,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
               (sigma,(k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst,
               evarsubst)
 	    else error_cannot_unify_local curenv sigma (m,n,cM)
+	| 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)
 	| Evar (evk,_ as ev), _
             when not (Evar.Set.mem evk flags.frozen_evars) 
 	      && not (occur_evar evk cN) ->
@@ -1673,11 +1677,13 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
 		 matchrec t
 	       with ex when precatchable_exception ex ->
 		 matchrec c)
+
           | Lambda (_,t,c) ->
 	      (try
 		 matchrec t
 	       with ex when precatchable_exception ex ->
 		 matchrec c)
+
           | _ -> error "Match_subterm"))
   in
   try matchrec cl
@@ -1774,7 +1780,12 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
           try
 	    (* This is up to delta for subterms w/o metas ... *)
 	    w_unify_to_subterm env evd ~flags (strip_outer_cast op,t)
-	  with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op)
+	  with PretypeError (env,_,NoOccurrenceFound _) when
+              allow_K ||
+                (* w_unify_to_subterm does not go through evars, so
+                   the next step, which was already in <= 8.4, is
+                   needed at least for compatibility of rewrite *)
+                dependent op t -> (evd,op)
         in
 	  if not allow_K &&
             (* ensure we found a different instance *)