- cicUtil: is_sober now detects folded applications

[helm.git] / helm / software / components / cic / cicUtil.ml

diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml
index 8fa9828590a604242c234bb25cf39cff3de17ce3..deb8f1e68bc3fdf69a84b4f3e5fc77d50d5f4515 100644 (file)
--- a/helm/software/components/cic/cicUtil.ml
+++ b/helm/software/components/cic/cicUtil.ml
@@ -565,7 +565,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