diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f894eb8fc..5406832d2 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2119,7 +2119,12 @@ and interp_atomic ist tac : unit Proofview.tactic = | AllOccurrences | NoOccurrences -> true | _ -> false in - let c_interp sigma = + let c_interp patvars sigma = + let lfun' = Id.Map.fold (fun id c lfun -> + Id.Map.add id (Value.of_constr c) lfun) + patvars ist.lfun + in + let ist = { ist with lfun = lfun' } in if is_onhyps && is_onconcl then interp_type ist (pf_env gl) sigma c else interp_constr ist (pf_env gl) sigma c @@ -2139,7 +2144,12 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma,sign,op) = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in let env' = Environ.push_named_context sign env in - let c_interp sigma = + let c_interp patvars sigma = + let lfun' = Id.Map.fold (fun id c lfun -> + Id.Map.add id (Value.of_constr c) lfun) + patvars ist.lfun + in + let ist = { ist with lfun = lfun' } in try interp_constr ist env' sigma c with e when to_catch e (* Hack *) -> errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") |