diff options
author | 2011-03-04 15:15:18 +0000 | |
---|---|---|
committer | 2011-03-04 15:15:18 +0000 | |
commit | 473f647d9d5200e5af182e4048f0949f5983774b (patch) | |
tree | 987f455fdd8f083b15cf5545f7341c1caf28fe42 /tactics/eauto.ml4 | |
parent | 0389da80801ad7f819db27702e849671185836c4 (diff) |
- Allow to set a particular transparent_state for the local hint
database
- Fix [specialize] to properly resolve typeclass constraints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13868 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/eauto.ml4')
-rw-r--r-- | tactics/eauto.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index ed8da10a0..59e7fcca1 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -291,7 +291,7 @@ let e_breadth_search debug n db_list local_db gl = with Not_found -> error "eauto: breadth first search failed." let e_search_auto debug (in_depth,p) lems db_list gl = - let local_db = make_local_hint_db true lems gl in + let local_db = make_local_hint_db ~ts:full_transparent_state true lems gl in if in_depth then e_depth_search debug p db_list local_db gl else |