prerr_endline => debug_print

[helm.git] / helm / software / components / metadata / metadataConstraints.ml

diff --git a/helm/software/components/metadata/metadataConstraints.ml b/helm/software/components/metadata/metadataConstraints.ml
index 73f137a432a5ac4bbb2323ebc239d00c1503d221..e35e35894978ac33651b9f7c3e17663b1ec8a72b 100644 (file)
--- a/helm/software/components/metadata/metadataConstraints.ml
+++ b/helm/software/components/metadata/metadataConstraints.ml
@@ -269,8 +269,9 @@ and inspect_conclusion n t =
        merge n (inspect_conclusion n s) (inspect_conclusion n t)
     | Cic.Lambda (_, s, t) ->
        merge n (inspect_conclusion n s) (inspect_conclusion n t)
-    | Cic.LetIn (_, s, t) ->
-       merge n (inspect_conclusion n s) (inspect_conclusion n t)
+    | Cic.LetIn (_, s, ty, t) ->
+       merge n (inspect_conclusion n s)
+       (merge n (inspect_conclusion n ty) (inspect_conclusion n t))
     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
        add_root (n-1) u l
     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
@@ -308,7 +309,7 @@ let rec inspect_term n t =
        Some uri, SetSet.empty
     | Cic.Cast (t, _) -> inspect_term n t
     | Cic.Prod (_, _, t) -> inspect_term n t
-    | Cic.LetIn (_, _, t) -> inspect_term n t
+    | Cic.LetIn (_, _, _, t) -> inspect_term n t
     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
        let childunion = inspect_children (n-1) l in
        Some u, childunion
@@ -396,8 +397,9 @@ and signature_concl =
        UriManagerSet.union (signature_concl s) (signature_concl t)
     | Cic.Lambda (_, s, t) ->
        UriManagerSet.union (signature_concl s) (signature_concl t)
-    | Cic.LetIn (_, s, t) ->
-       UriManagerSet.union (signature_concl s) (signature_concl t)
+    | Cic.LetIn (_, s, ty, t) ->
+       UriManagerSet.union (signature_concl s)
+       (UriManagerSet.union (signature_concl ty) (signature_concl t))
     | Cic.Appl l  -> add l
     | Cic.MutCase _
     | Cic.Fix _
@@ -407,7 +409,7 @@ and signature_concl =
 let rec signature_of = function
   | Cic.Cast (t, _)      -> signature_of t
   | Cic.Prod (_, _, t)   -> signature_of t               
-  | Cic.LetIn (_, _, t) -> signature_of t
+  | Cic.LetIn (_, _, _, t) -> signature_of t
   | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
       Some (u, []), add l
   | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->