From fd19fbb3720f1f1d930dcd082ddcd021cb6e8b50 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Apr 2015 16:50:38 +0200
Subject: Remove evars in the type of _unnammed_ metas in pattern_of_constr
 (fixes QuicksortComplexity).

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

(limited to 'pretyping')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 009b7323e4..9fb6ec9d11 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -171,7 +171,10 @@ let pattern_of_constr env sigma t =
           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
+	 remove := Evar.Set.union (evars_of_term ty) !remove;
+	 PMeta None)
     | Case (ci,p,a,br) ->
         let cip =
 	  { cip_style = ci.ci_pp_info.style;
-- 
cgit v1.2.3


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')

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