X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUtil.ml;h=36f65391eeac23d27c565b65d8e09ea52cd22f0c;hb=a232a59672817abd3d6ec07db0b20d8b3fe5ad3b;hp=8fa9828590a604242c234bb25cf39cff3de17ce3;hpb=84e6cbe962c9a534be48542c098d7bb0d90be9a1;p=helm.git

diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml
index 8fa982859..36f65391e 100644
--- a/helm/software/components/cic/cicUtil.ml
+++ b/helm/software/components/cic/cicUtil.ml
@@ -550,7 +550,8 @@ let alpha_equivalence =
 
 let is_sober c t =
    let rec sober_term c g = function
-      | C.Rel _ 
+      | C.Rel i                         ->
+         if i <= 0 then fun b -> false else g
       | C.Sort _  
       | C.Implicit _                    -> g      
       | C.Const (_, xnss) 
@@ -565,7 +566,8 @@ let is_sober c t =
       | C.LetIn (_, v, ty, t)           ->
          sober_term c (sober_term c (sober_term c g t) ty) v
       | C.Appl []                       
-      | C.Appl [_]                      -> fun b -> false
+      | C.Appl [_]                      
+      | C.Appl (C.Appl _ :: _)          -> fun b -> false
       | C.Appl ts                       -> sober_terms c g ts
       | C.MutCase (_, _, t, v, ts)      -> 
          sober_terms c (sober_term c (sober_term c g t) v) ts