diff options
| author | herbelin | 2005-03-08 22:04:18 +0000 |
|---|---|---|
| committer | herbelin | 2005-03-08 22:04:18 +0000 |
| commit | 845bd29d5705bae113afed6f5b8fd3195fb6b0fd (patch) | |
| tree | b8055d9d223bccdc1b48cd7cdc59ebcfb3dda737 /tactics | |
| parent | b2a962c342c74e96dc81e9eca30515282864620c (diff) | |
Fix bug #931: leave dependent evars as such for refine
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6812 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/refine.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/refine.ml b/tactics/refine.ml index db4c52020b..d53310c669 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -337,8 +337,8 @@ let rec tcc_aux subst (TH (c,mm,sgp) as th) gl = let refine oc gl = let sigma = project gl in - let (_gmm,c) = Evarutil.exist_to_meta sigma oc in - (* Relies on Cast's put on Meta's by exist_to_meta, because it is otherwise - complicated to update gmm when passing through a binder *) + let (sigma,c) = Evarutil.evars_to_metas sigma oc in + (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise + complicated to update meta types when passing through a binder *) let th = compute_metamap (pf_env gl) c in - tcc_aux [] th gl + tclTHEN (Refiner.tclEVARS sigma) (tcc_aux [] th) gl |