Matitaweb:

[helm.git] / matitaB / components / content_pres / content2presMatcher.ml

diff --git a/matitaB/components/content_pres/content2presMatcher.ml b/matitaB/components/content_pres/content2presMatcher.ml
index 5eeed2667689d7e830bff041654d1bf1bee331ad..0020f8170cdcb836d5ccb0cfd43a4706f00fec4b 100644 (file)
--- a/matitaB/components/content_pres/content2presMatcher.ml
+++ b/matitaB/components/content_pres/content2presMatcher.ml
@@ -183,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