diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-18 18:17:16 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-18 18:17:16 +0000 |
| commit | 4cb5880d9f3afa0b92eeb49a1295341da3769f81 (patch) | |
| tree | b74f3cb3d6bb3927556fef2a09253f2b63baf5e3 /tactics/class_tactics.ml4 | |
| parent | 8cf4e04fa817cf7ff9d73cb5cb7fff8b3b950387 (diff) | |
Fixed bug #1966, wrong handling of evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11468 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/class_tactics.ml4')
| -rw-r--r-- | tactics/class_tactics.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index c7cebd110..662f2ac58 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -1045,9 +1045,9 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g | None -> (sort, inverse sort impl) | Some _ -> (sort, impl) in - let evars = ref (Evd.create_evar_defs Evd.empty) in - let env = pf_env gl in let sigma = project gl in + let evars = ref (Evd.create_evar_defs sigma) in + let env = pf_env gl in let eq = build_new gl env sigma flags occs hypinfo concl (Some (Lazy.lazy_from_val cstr)) evars in match eq with @@ -1084,7 +1084,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g mkApp (p, [| mkRel 2 |]))), [| mkMeta goal_meta; t |]))) in - let evartac = + let evartac = let evd = Evd.evars_of undef in if not (evd = Evd.empty) then Refiner.tclEVARS (Evd.merge sigma evd) else tclIDTAC |