From 9a16dd4b0e536cadf32c024c5bb406290e28922b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 15 Apr 2001 01:50:47 +0000
Subject: Mise en page

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

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6f76482931..ca64a856ec 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1251,7 +1251,7 @@ let sub_term_with_unif cref ceq =
           else
             Some (ceq,nb_occ)
     |Some (head,t_args) ->
-        let (l,nb)=find_match [] 0 head t_args cref in
+        let (l,nb) = find_match [] 0 head t_args cref in
         if nb = 0 then
           None
         else
@@ -1278,9 +1278,7 @@ let general_rewrite_in lft2rgt id (c,lb) gls =
           else
             List.hd (List.rev l)
         in
-        (match (sub_term_with_unif 
-		  (collapse_appl (strip_outer_cast typ_id))
-		  (collapse_appl mbr_eq)) with
+        (match sub_term_with_unif typ_id mbr_eq with
            | None ->
                errorlabstrm "general_rewrite_in" 
 		 [<'sTR "Nothing to rewrite in: "; pr_id id>]
-- 
cgit v1.2.3