guarded by has a nice error message

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

diff --git a/helm/software/components/metadata/metadataExtractor.ml b/helm/software/components/metadata/metadataExtractor.ml
index 4fbae1ba76ed43238afdc7cfb51b1d0fd329bf65..462679534c0488e1e4aa97a2255cb4b305fb34d4 100644 (file)
--- 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) ->