From 06bd5357554ce06079b33288d3b9be0e68b44302 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 26 Jan 2010 16:51:00 +0000
Subject: Quick fix for references to section variables unbound in the current
 environment during unification. Should be checked earlier.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12692 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/unification.ml  | 2 +-
 tactics/class_tactics.ml4 | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 9156dfa9e2..d26195efc8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -177,7 +177,7 @@ let use_evars_pattern_unification flags =
 
 let expand_key env = function
   | Some (ConstKey cst) -> constant_opt_value env cst
-  | Some (VarKey id) -> named_body id env
+  | Some (VarKey id) -> (try named_body id env with Not_found -> None)
   | Some (RelKey _) -> None
   | None -> None
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index b77425f0d6..45e6884566 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -523,7 +523,8 @@ exception FoundTerm of constr
 
 let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
   let gls = { it = Evd.make_evar (Environ.named_context_val env) gl; sigma = sigma } in
-  let gls', v = eauto [searchtable_map typeclasses_db] gls in
+  let hints = searchtable_map typeclasses_db in
+  let gls', v = eauto ~st:(Hint_db.transparent_state hints) [hints] gls in
   let term = v [] in
   let evd = sig_sig gls' in
   let term = fst (Refiner.extract_open_proof evd term) in
-- 
cgit v1.2.3