From 6e0c5c81e9e81c2e5369427643b2ac51b9aa17e6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 17 Oct 2014 15:41:54 +0200
Subject: Revert "Fixing a loop in proof reconstruction for congruence
 (#2447)." committed by mistake. The message pretended to have a fix which is
 only superficially a fix. The problem is more complex.

This reverts commit 251218905daea0838a3738466afa1c278bb3e81b.
---
 plugins/cc/ccproof.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index ba449e76d7..6177f22f3b 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -116,7 +116,7 @@ let build_proof uf=
     in  ptrans (ptrans pi pij) pj
 
   and constr_proof i t ipac=
-    if ipac.args=[] || i=t then
+    if ipac.args=[] then
       equal_proof i t
     else
       let npac=tail_pac ipac in
-- 
cgit v1.2.3