meta VS meta in alpha_eq honors substitution

[helm.git] / helm / software / components / content_pres / termContentPres.ml

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index d68b6a8b4bfee412eab2ac206acb46aab90f55cd..0f51e36a9acf9fb2241017a0a12580bdccb5a72d 100644 (file)
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -204,7 +204,8 @@ let pp_ast0 t k =
             hvbox false true [
               keyword "let"; space;
               hvbox false true [
-                aux_var var; space; builtin_symbol "\\def"; break; top_pos (k s) ];
+                aux_var var; space;
+                builtin_symbol "\\def"; break; top_pos (k s) ];
               break; space; keyword "in" ];
             break;
             k t ])
@@ -550,8 +551,8 @@ let instantiate_level2 env term =
     | Ast.Case (term, indty, outty_opt, patterns) ->
         Ast.Case (aux env term, indty, aux_opt env outty_opt,
           List.map (aux_branch env) patterns)
-    | Ast.LetIn (var, t1, t2) ->
-        Ast.LetIn (aux_capture_var env var, aux env t1, aux env t2)
+    | Ast.LetIn (var, t1, t3) ->
+        Ast.LetIn (aux_capture_var env var, aux env t1, aux env t3)
     | Ast.LetRec (kind, definitions, body) ->
         Ast.LetRec (kind, List.map (aux_definition env) definitions,
           aux env body)