Merge branch 'v8.5'

1 files changed, 5 insertions, 2 deletions

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 009b7323e4..705e594af1 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -167,11 +167,14 @@ let pattern_of_constr env sigma t =
       | Evar_kinds.MatchingVar (b,id) ->
 	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
           ctx := (id,None,ty)::!ctx;
-	  keep := Evar.Set.union (evars_of_term ty) !keep;
+	  let () = ignore (pattern_of_constr env ty) in
           assert (not b); PMeta (Some id)
       | Evar_kinds.GoalEvar -> 
 	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
-      | _ -> PMeta None)
+      | _ -> 
+	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+	let () = ignore (pattern_of_constr env ty) in
+	 PMeta None)
     | Case (ci,p,a,br) ->
         let cip =
 	  { cip_style = ci.ci_pp_info.style;