From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 19 May 2008 23:31:21 +0000 (+0000)
Subject: Code simplification.
X-Git-Tag: make_still_working~5140
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5367ccdfa9f7c748b179c788979fb4a340932987;p=helm.git

Code simplification.
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index c028b916f..1a899aaaa 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1013,8 +1013,7 @@ and type_of_constant ((Ref.Ref (uri,_)) as ref) =
  in
   match E.get_checked_obj uri, ref with
   | (_,_,_,_,C.Inductive(isind1,lno1,tl,_)),Ref.Ref(_,Ref.Ind (isind2,i,lno2))->
-      if isind1 <> isind2 then error ();
-      if lno1 <> lno2 then error ();
+      if isind1 <> isind2 || lno1 <> lno2 then error ();
       let _,_,arity,_ = List.nth tl i in arity
   | (_,_,_,_,C.Inductive (_,lno1,tl,_)), Ref.Ref (_,Ref.Con (i,j,lno2))  ->
       if lno1 <> lno2 then error ();