From 72b9a7df489ea47b3e5470741fd39f6100d31676 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Sat, 18 Aug 2007 20:34:57 +0000
Subject: Imported Upstream version 8.1.pl1+dfsg

---
 proofs/logic.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 92225948..0846997e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 9601 2007-02-06 21:37:59Z herbelin $ *)
+(* $Id: logic.ml 9805 2007-04-28 21:28:37Z herbelin $ *)
 
 open Pp
 open Util
@@ -582,10 +582,10 @@ let subst_proof_vars =
          
 let rec rebind id1 id2 = function
   | [] -> [Name id2,SectionVar id1]
-  | (na,_ as x)::l -> 
-      if na = Name id1 then (Name id2,ProofVar)::l else
+  | (na,k as x)::l -> 
+      if na = Name id1 then (Name id2,k)::l else
         let l' = rebind id1 id2 l in
-        if na = Name id2 then (Anonymous,ProofVar)::l' else x::l'
+        if na = Name id2 then (Anonymous,k)::l' else x::l'
 
 let add_proof_var id vl = (Name id,ProofVar)::vl
 
-- 
cgit v1.2.3