From f973052543cdd0f4c98366a7c2eefabeaf138afa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Apr 2015 17:32:36 +0200
Subject: Really fix constr_of_pattern and bugs #3590 and #4120 by removing all
 evars appearing in the constr (or their types, recursively) from the
 evar_map.

---
 pretyping/patternops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/patternops.ml')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 9fb6ec9d11..705e594af1 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -167,13 +167,13 @@ 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)
       | _ -> 
 	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
-	 remove := Evar.Set.union (evars_of_term ty) !remove;
+	let () = ignore (pattern_of_constr env ty) in
 	 PMeta None)
     | Case (ci,p,a,br) ->
         let cip =
-- 
cgit v1.2.3