Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13179 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 0 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index cf788f36d..1f944587e 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -605,6 +605,13 @@ let extract_all_conv_pbs evd =
 let evar_merge evd evars =
   { evd with evars = EvarMap.merge evd.evars evars.evars }
 
+let evar_list evd c =
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (evk, _ as ev) when mem evd evk -> ev :: acc
+    | _ -> fold_constr evrec acc c in
+  evrec [] c
+
 (**********************************************************)
 (* Sort variables *)