]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/cicNotationUtil.ml
print the name not found in the env
[helm.git] / helm / software / components / acic_content / cicNotationUtil.ml
index 99aafa44051765813c6f198ad71cd7945a626cbc..51acf758f080d427cb43ff4370a00b0c63eba833 100644 (file)
@@ -35,8 +35,8 @@ let visit_ast ?(special_k = fun _ -> assert false) k =
     | Ast.Case (term, indtype, typ, patterns) ->
         Ast.Case (k term, indtype, aux_opt typ, aux_patterns patterns)
     | Ast.Cast (t1, t2) -> Ast.Cast (k t1, k t2)
-    | Ast.LetIn (var, t1, t2) ->
-        Ast.LetIn (aux_capture_variable var, k t1, k t2)
+    | Ast.LetIn (var, t1, t3) ->
+        Ast.LetIn (aux_capture_variable var, k t1, k t3)
     | Ast.LetRec (kind, definitions, term) ->
         let definitions =
           List.map
@@ -187,9 +187,9 @@ let meta_names_of_term term =
         aux term ;
         aux_opt outty_opt ;
         List.iter aux_branch patterns
-    | Ast.LetIn (_, t1, t2) ->
+    | Ast.LetIn (_, t1, t3) ->
         aux t1 ;
-        aux t2
+        aux t3
     | Ast.LetRec (_, definitions, body) ->
         List.iter aux_definition definitions ;
         aux body