X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2Fcontent2presMatcher.ml;h=0020f8170cdcb836d5ccb0cfd43a4706f00fec4b;hb=2f19651bcec24abfb1bf15ff7e1387daad1f6638;hp=a7b59aa52e3c3a3346f555aa1f3c3323ed53e993;hpb=1b67bd4dfa12ef25b8fa63884c71893b961db27d;p=helm.git

diff --git a/matitaB/components/content_pres/content2presMatcher.ml b/matitaB/components/content_pres/content2presMatcher.ml
index a7b59aa52..0020f8170 100644
--- a/matitaB/components/content_pres/content2presMatcher.ml
+++ b/matitaB/components/content_pres/content2presMatcher.ml
@@ -71,8 +71,9 @@ struct
 
     (* Debugging only *)
     (*CSC: new NCicPp.status is the best I can do now *)
-    let string_of_term = NotationPp.pp_term (new NCicPp.status)
-    let string_of_pattern = NotationPp.pp_term (new NCicPp.status)
+    (*WR: can't guess a user id so I must use None *)
+    let string_of_term = NotationPp.pp_term (new NCicPp.status None)
+    let string_of_pattern = NotationPp.pp_term (new NCicPp.status None)
   end
 
   module M = PatternMatcher.Matcher (Pattern21)
@@ -182,19 +183,19 @@ struct
                        let env'' = Env.remove_name env' acc_name in
 			 match aux acc with
 			   | None -> aux_base term
-			   | Some (base_env, ctors', rec_envl) -> 
-                               let ctors'' = ctors' @ ctors in
+			   | Some (base_env, ctors_acc, rec_envl) -> 
+                               let ctors'' = ctors' @ ctors_acc (* @ ctors *)in
 			       Some (base_env, ctors'',env'' :: rec_envl)
                      end
 	     in
                match aux term with
 		 | None -> None
-		 | Some (base_env, ctors, rec_envl) ->
+		 | Some (base_env, ctors_term, rec_envl) ->
                      let env' =
                        base_env @ Env.coalesce_env p_rec_decls rec_envl @ env
                        (* @ env LUCA!!! *)
                      in
-                     Some (env', ctors))
+                     Some (env', ctors_term @ ctors))
 
     | Ast.Default (p_some, p_none) ->  (* p_none can't bound names *)
         let p_some_decls = Env.declarations_of_term p_some in