X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fmetadata%2FmetadataExtractor.ml;h=462679534c0488e1e4aa97a2255cb4b305fb34d4;hb=bc698deb9b8416c2b903b78a6053d59f6cc2a8ec;hp=4fbae1ba76ed43238afdc7cfb51b1d0fd329bf65;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/metadata/metadataExtractor.ml b/helm/software/components/metadata/metadataExtractor.ml
index 4fbae1ba7..462679534 100644
--- a/helm/software/components/metadata/metadataExtractor.ml
+++ b/helm/software/components/metadata/metadataExtractor.ml
@@ -119,7 +119,7 @@ let compute_term pos term =
         (*assert (not (is_main_pos pos));*)
         let set = aux (next_pos pos) set source in
         aux (next_pos pos) set target
-    | Cic.LetIn (_, term, target) ->
+    | Cic.LetIn (_, term, _, target) ->
         if is_main_pos pos then
           aux pos set (CicSubstitution.subst term target)
         else
@@ -210,7 +210,7 @@ let compute_metas term =
     | Cic.Lambda (_, source, target) ->
         let acc = aux in_hyp acc source in
         aux in_hyp acc target
-    | Cic.LetIn (_, term, target) ->
+    | Cic.LetIn (_, term, _, target) ->
         aux in_hyp acc (CicSubstitution.subst term target)
     | Cic.Appl [] -> assert false
     | Cic.Appl (hd :: tl) ->