X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=0f51e36a9acf9fb2241017a0a12580bdccb5a72d;hb=08e9d02504942642a917c0d3e4b4795e65172d89;hp=0ee424f18570d318b74d942d936573029d206eed;hpb=87bdd061d096c836a02c77aa26e80d9c36180fad;p=helm.git

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 0ee424f18..0f51e36a9 100644
--- 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 ])
@@ -468,8 +469,9 @@ let fill_pos_info l1_pattern = l1_pattern
   in
   aux true l1_pattern *)
 
+let counter = ref ~-1 
+let reset () = counter := ~-1;;
 let fresh_id =
-  let counter = ref ~-1 in
   fun () ->
     incr counter;
     !counter
@@ -549,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)
@@ -672,3 +674,5 @@ let instantiate_level2 env term =
 
 let _ = load_patterns21 []
 
+
+