diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-04-13 16:40:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-04-13 16:40:16 +0200 |
| commit | 546e2454f244340694f8fca460598499359afe28 (patch) | |
| tree | caa4448d72abd0df4c4995d20060654a152f1897 /tactics | |
| parent | 781a0f13667bedc6f1c1ec64266c0dc90b1b23b5 (diff) | |
Remove declarations of matched variables in change as an extension of
the context... overlooked by my last commit. Fixes relation-algebra.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 5406832d2..f29680e18 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2143,14 +2143,13 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.V82.tactic begin fun gl -> 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 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 + 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.") in |