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/patternops.ml')

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