From 546e2454f244340694f8fca460598499359afe28 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 13 Apr 2015 16:40:16 +0200
Subject: Remove declarations of matched variables in change as an extension of
 the context... overlooked by my last commit. Fixes relation-algebra.

---
 tactics/tacinterp.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5406832d2f..f29680e185 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
-- 
cgit v1.2.3