diff options
| author | ppedrot | 2012-12-14 09:26:08 +0000 |
|---|---|---|
| committer | ppedrot | 2012-12-14 09:26:08 +0000 |
| commit | 9330bf650ca602884c5c4c69c2fb3e94ee32838b (patch) | |
| tree | 5947d599c9c408680236995b11a47ab93703b701 /toplevel/command.ml | |
| parent | 02077f5b5e132e135be778c201e74a5eb87b97ae (diff) | |
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
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 12 |
1 files changed, 1 insertions, 11 deletions
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 |