Implicit annotationas are now printed

[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 75b7fd2cc8505390ec0ff96cc203d9744fd5b390..8c42aed6131a5348fb542f580eb1422f423d87e8 100644 (file)
--- a/helm/software/components/cic/cicUtil.ml
+++ b/helm/software/components/cic/cicUtil.ml
@@ -557,43 +557,44 @@ let alpha_equivalence =
   in
    aux
 
-let is_sober t =
-   let rec sober_term g = function
+let is_sober c t =
+   let rec sober_term c g = function
       | C.Rel _ 
       | C.Sort _  
       | C.Implicit _                    -> g      
       | C.Const (_, xnss) 
       | C.Var (_, xnss) 
       | C.MutConstruct (_, _, _, xnss)
-      | C.MutInd (_, _, xnss)           -> sober_xnss g xnss
-      | C.Meta (_, xss)                 -> sober_xss g xss
+      | C.MutInd (_, _, xnss)           -> sober_xnss c g xnss
+      | C.Meta (_, xss)                 -> sober_xss c g xss
       | C.Lambda (_, v, t)
       | C.Prod (_, v, t)
-      | C.Cast (t, v)                   -> sober_term (sober_term g t) v
-      | C.LetIn (_, v, ty, t)           -> sober_term
-                                            (sober_term (sober_term g t) ty) v
+      | C.Cast (t, v)                   ->
+         sober_term c (sober_term c g t) v
+      | 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 ts                       -> sober_terms g ts
+      | C.Appl ts                       -> sober_terms c g ts
       | C.MutCase (_, _, t, v, ts)      -> 
-         sober_terms (sober_term (sober_term g t) v) ts
-      | C.Fix (_, ifs)                  -> sober_ifs g ifs
-      | C.CoFix (_, cifs)               -> sober_cifs g cifs
-   and sober_terms g = List.fold_left sober_term g
-   and sober_xnss g =
-      let map g (_, t) = sober_term g t in
+         sober_terms c (sober_term c (sober_term c g t) v) ts
+      | C.Fix (_, ifs)                  -> sober_ifs c g ifs
+      | C.CoFix (_, cifs)               -> sober_cifs c g cifs
+   and sober_terms c g = List.fold_left (sober_term c) g
+   and sober_xnss c g =
+      let map g (_, t) = sober_term c g t in
       List.fold_left map g
-   and sober_xss g =
+   and sober_xss c g =
       let map g = function 
          | None   -> g
-        | Some t -> sober_term g t
+        | Some t -> sober_term c g t
       in
       List.fold_left map g
-   and sober_ifs g =
-      let map g (_, _, t, v) = sober_term (sober_term g t) v in
+   and sober_ifs c g =
+      let map g (_, _, t, v) = sober_term c (sober_term c g t) v in
       List.fold_left map g
-   and sober_cifs g =
-      let map g (_, t, v) = sober_term (sober_term g t) v in
+   and sober_cifs c g =
+      let map g (_, t, v) = sober_term c (sober_term c g t) v in
       List.fold_left map g
    in 
-   sober_term (fun b -> b) t true
+   sober_term c (fun b -> b) t true