From 9330bf650ca602884c5c4c69c2fb3e94ee32838b Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 14 Dec 2012 09:26:08 +0000
Subject: Implemented a full-fledged equality on [constr_expr]. By the way,
 some cleaning of the interface and moving of code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16066 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

(limited to 'toplevel/command.ml')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 5967b435a3..69918b2b0a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -328,18 +328,8 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
     impls
 
 (* Very syntactical equality *)
-let eq_local_binder d1 d2 = match d1,d2 with
-  | LocalRawAssum (nal1,k1,c1), LocalRawAssum (nal2,k2,c2) ->
-      Int.equal (List.length nal1) (List.length nal2) && binder_kind_eq k1 k2 &&
-      List.for_all2 (fun (_,na1) (_,na2) -> name_eq na1 na2) nal1 nal2 &&
-      Constrextern.is_same_type c1 c2
-  | LocalRawDef ((_,id1),c1), LocalRawDef ((_,id2),c2) ->
-      name_eq id1 id2 && Constrextern.is_same_type c1 c2
-  | _ ->
-      false
-
 let eq_local_binders bl1 bl2 =
-  Int.equal (List.length bl1) (List.length bl2) && List.for_all2 eq_local_binder bl1 bl2
+  List.equal local_binder_eq bl1 bl2
 
 let extract_coercions indl =
   let mkqid (_,((_,id),_)) = qualid_of_ident id in
-- 
cgit v1.2.3