From c14986c2fa8c8563f7da68d98b7c0b7f6ea2c9e7 Mon Sep 17 00:00:00 2001
From: glondu
Date: Wed, 28 Oct 2009 16:48:36 +0000
Subject: Remove old compatibility stuff (Tacred.nf)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12436 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 200b6deb71..9957e8a393 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -919,8 +919,8 @@ let try_delta_expand env sigma t =
 let simplify_args env sigma t =
   (* Quick hack to reduce in arguments of eq only *)
   match decompose_app t with
-    | eq, [t;c1;c2] -> applist (eq,[t;nf env sigma c1;nf env sigma c2])
-    | eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2])
+    | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma c1;simpl env sigma c2])
+    | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2])
     | _ -> t
 
 let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns tac =
-- 
cgit v1.2.3